86 static char rcsid[]
DD_UNUSED =
"$Id: cuddAddIte.c,v 1.16 2012/02/05 01:07:18 fabio Exp $";
135 DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
136 unsigned int topf,topg,toph,v;
140 if (f == (one =
DD_ONE(dd))) {
143 if (f == (zero =
DD_ZERO(dd))) {
161 v =
ddMin(topg,toph);
231 DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
232 unsigned int topf,topg;
243 if (f == (zero =
DD_ZERO(dd))) {
346 DdNode *tmp, *fv, *fvn, *gv, *gvn;
347 unsigned int topf, topg, res;
350 if (f == g)
return(1);
364 return(tmp ==
DD_ONE(dd));
417 DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
418 unsigned int topf,topg,toph,v;
425 if (f == (one =
DD_ONE(dd))) {
428 if (f == (zero =
DD_ZERO(dd))) {
441 if (h == zero)
return(f);
447 v =
ddMin(topg,toph);
450 if (topf < v &&
cuddT(f) == one &&
cuddE(f) == zero) {
454 if (topf < v &&
cuddT(f) == zero &&
cuddE(f) == one) {
488 if (t == NULL)
return(NULL);
552 if (t == NULL)
return(NULL);
683 #define JUMP_UP_PROB 0.36 684 #define MAXGEN_RATIO 15.0 685 #define STOP_TEMP 1.0 707 extern int ddTotalNISwaps;
709 static int acceptances;
773 double NewTemp, temp;
775 int innerloop, maxGen;
776 int ecount, ucount, dcount;
778 nvars = upper - lower + 1;
782 (void) fprintf(table->
out,
"\n");
784 if (result == 0)
return(0);
790 BestOrder =
ALLOC(
int,nvars);
791 if (BestOrder == NULL) {
804 ecount = ucount = dcount = 0;
808 (void) fprintf(table->
out,
"temp=%f\tsize=%d\tgen=%d\t",
810 tosses = acceptances = 0;
812 for (innerloop = 0; innerloop < maxGen; innerloop++) {
832 (void) fprintf(table->
out,
833 "Exchange of %d and %d: size = %d\n",
840 (void) fprintf(table->
out,
841 "Jump up of %d to %d: size = %d\n",
848 (void) fprintf(table->
out,
849 "Jump down of %d to %d: size = %d\n",
860 if (size < BestCost) {
869 NewTemp =
ALPHA * temp;
870 if (NewTemp >= 1.0) {
871 maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
875 (void) fprintf(table->
out,
"uphill = %d\taccepted = %d\n",
883 if (!result)
return(0);
885 fprintf(table->
out,
"#:N_EXCHANGE %8d : total exchanges\n",ecount);
886 fprintf(table->
out,
"#:N_JUMPUP %8d : total jumps up\n",ucount);
887 fprintf(table->
out,
"#:N_JUMPDOWN %8d : total jumps down",dcount);
921 }
else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
973 int initial_size, limit_size;
981 initial_size = limit_size = table->
keys - table->
isolated;
984 if (x_next == y_next) {
986 if (size == 0)
goto ddExchangeOutOfMem;
988 if (move == NULL)
goto ddExchangeOutOfMem;
995 if (size == 0)
goto ddExchangeOutOfMem;
997 if (move == NULL)
goto ddExchangeOutOfMem;
1004 if (size == 0)
goto ddExchangeOutOfMem;
1006 if (move == NULL)
goto ddExchangeOutOfMem;
1016 }
else if (x == y_next) {
1018 if (size == 0)
goto ddExchangeOutOfMem;
1020 if (move == NULL)
goto ddExchangeOutOfMem;
1031 if (size == 0)
goto ddExchangeOutOfMem;
1033 if (move == NULL)
goto ddExchangeOutOfMem;
1040 if (size == 0)
goto ddExchangeOutOfMem;
1042 if (move == NULL)
goto ddExchangeOutOfMem;
1054 if (x_next > y_ref)
break;
1058 }
else if (size < limit_size) {
1063 if (y_next>=x_ref) {
1065 if (size == 0)
goto ddExchangeOutOfMem;
1067 if (move == NULL)
goto ddExchangeOutOfMem;
1077 if (!result)
goto ddExchangeOutOfMem;
1079 while (moves != NULL) {
1087 while (moves != NULL) {
1135 if (moves == NULL)
goto ddJumpingAuxOutOfMem;
1138 if (!result)
goto ddJumpingAuxOutOfMem;
1142 if (moves == NULL)
goto ddJumpingAuxOutOfMem;
1145 if (!result)
goto ddJumpingAuxOutOfMem;
1147 (void) fprintf(table->
err,
"Unexpected condition in ddJumping\n");
1148 goto ddJumpingAuxOutOfMem;
1150 while (moves != NULL) {
1157 ddJumpingAuxOutOfMem:
1158 while (moves != NULL) {
1192 int limit_size = initial_size;
1196 while (y >= x_low) {
1198 if (size == 0)
goto ddJumpingUpOutOfMem;
1200 if (move == NULL)
goto ddJumpingUpOutOfMem;
1206 if ((
double) size > table->
maxGrowth * (double) limit_size) {
1208 }
else if (size < limit_size) {
1216 ddJumpingUpOutOfMem:
1217 while (moves != NULL) {
1251 int limit_size = initial_size;
1255 while (y <= x_high) {
1257 if (size == 0)
goto ddJumpingDownOutOfMem;
1259 if (move == NULL)
goto ddJumpingDownOutOfMem;
1265 if ((
double) size > table->
maxGrowth * (double) limit_size) {
1267 }
else if (size < limit_size) {
1275 ddJumpingDownOutOfMem:
1276 while (moves != NULL) {
1309 int best_size = size;
1310 double coin, threshold;
1313 for (move = moves; move != NULL; move = move->
next) {
1314 if (move->
size < best_size) {
1315 best_size = move->
size;
1323 if (best_size == size) {
1328 threshold = exp(-((
double)(table->
keys - table->
isolated - size))/temp);
1329 if (coin < threshold) {
1341 for (move = moves; move != NULL; move = move->
next) {
1342 if (res == best_size)
return(1);
1344 if (!res)
return(0);
1374 nvars = upper - lower + 1;
1375 for (i = 0; i < nvars; i++) {
1376 array[i] = table->
invperm[i+lower];
1402 int nvars = upper - lower + 1;
1404 for (i = 0; i < nvars; i++) {
1405 x = table->
perm[array[i]];
1407 assert(x >= lower && x <= upper);
1410 while (y >= i + lower) {
1412 if (size == 0)
return(0);
1769 dd->
minHit = (double) hr / (100.0 - (
double) hr);
1810 if (dd->
tree != NULL) {
1834 if (dd->
treeZ != NULL) {
1864 if (i < 0 || i >= dd->
size)
return(-1);
1865 return(dd->
perm[i]);
1954 #ifndef DD_NO_DEATH_ROW 1958 count = (long) (dd->
keys - dd->
dead);
1963 for (i=0; i < dd->
size; i++) {
1964 if (dd->
vars[i]->
ref == 1) count--;
1967 if (
DD_ZERO(dd)->ref == 1) count--;
1996 DdHook **hook, *nextHook;
2015 while (nextHook != NULL) {
2016 if (nextHook->
f == f) {
2017 *hook = nextHook->
next;
2021 hook = &(nextHook->
next);
2022 nextHook = nextHook->
next;
2048 if (index >= dd->
size || index < 0)
return -1;
2071 if (index >= dd->
size || index < 0)
return(-1);
2100 if (index >= dd->
size || index < 0)
return(-1);
2132 treenode->
low = ((int) treenode->
index < size) ?
2134 if (treenode->
child != NULL)
2136 if (treenode->
younger != NULL)
2176 int startV, stopV, startL;
2180 while (auxnode != NULL) {
2181 if (auxnode->
child != NULL) {
2185 startV = dd->
permZ[auxnode->
index] / multiplicity;
2186 startL = auxnode->
low / multiplicity;
2187 stopV = startV + auxnode->
size / multiplicity;
2189 for (i = startV, j = startL; i < stopV; i++) {
2190 if (vmask[i] == 0) {
2192 while (lmask[j] == 1) j++;
2193 node =
Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
2339 (void) fprintf(manager->
err,
2340 "Error: Can only abstract positive cubes\n");
2375 unsigned topf, level;
2385 level = (
unsigned) dd->
perm[var->
index];
2396 return(res != zero);
2403 if (topf == level) {
2442 DdNode *F, *T, *E, *res, *res1, *res2, *
one;
2449 if (cube == one || F == one) {
2457 if (cube == one)
return(f);
2473 if (T == one || E == one || T ==
Cudd_Not(E)) {
2477 if (res1 == NULL)
return(NULL);
2506 if (res1 == NULL)
return(NULL);
2553 DdNode *F, *fv, *fnv, *G, *gv, *gnv;
2555 unsigned int topf, topg, topcube, top, index;
2605 top =
ddMin(topf, topg);
2608 if (topcube < top) {
2637 if (topcube == top) {
2644 if (t == NULL)
return(NULL);
2649 if (t == one && topcube == top) {
2662 if (topcube == top) {
2674 }
else if (t == e) {
2724 DdNode *T, *E, *res, *res1, *res2;
2752 if (res1 == NULL)
return(NULL);
2796 if (cube ==
DD_ONE(manager))
return(1);
2980 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
2984 unsigned int topf, topg, toph, v;
3017 v =
ddMin(topg, toph);
3020 if (topf < v &&
cuddT(f) == one &&
cuddE(f) == zero) {
3153 unsigned int saveLimit = dd->
maxLive;
3221 unsigned int saveLimit = dd->
maxLive;
3289 unsigned int topf, topg, res;
3293 if (f == g)
return(1);
3314 if (g == one)
return(1);
3315 if (f == one)
return(0);
3318 if (f == zero)
return(1);
3387 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
3388 unsigned int topf, topg, toph, v;
3396 if (f == (one =
DD_ONE(dd)))
3403 if (g == one || f == g) {
3410 }
else if (g == zero || f ==
Cudd_Not(g)) {
3418 if (h == zero || f == h) {
3421 }
else if (h == one || f ==
Cudd_Not(h)) {
3439 v =
ddMin(topg, toph);
3442 if (topf < v &&
cuddT(f) == one &&
cuddE(f) == zero) {
3481 if (t == NULL)
return(NULL);
3525 DdNode *fv, *fnv, *gv, *gnv;
3527 unsigned int index, topf, topg;
3534 if (f == zero || g == zero || f ==
Cudd_Not(g))
return(zero);
3535 if (f == g || g == one)
return(f);
3536 if (f == one)
return(g);
3539 if (f > g) {
DdNode *tmp = f; f = g; g = tmp; }
3541 if (res != NULL)
return(res);
3578 if (t == NULL)
return(NULL);
3638 DdNode *F, *fv, *fnv, *G, *gv, *gnv;
3640 unsigned int topf, topg, index;
3649 if (f == g)
return(f);
3653 if (f == one)
return(g);
3657 if (g == one)
return(f);
3671 if (F->
ref != 1 || G->
ref != 1) {
3673 if (r != NULL)
return(r);
3708 if (t == NULL)
return(NULL);
3740 if (F->
ref != 1 || G->
ref != 1)
3766 DdNode *fv, *fnv, *G, *gv, *gnv;
3768 unsigned int topf, topg, index;
3775 if (f == g)
return(zero);
3782 if (g == zero)
return(f);
3795 if (r != NULL)
return(r);
3826 if (t == NULL)
return(NULL);
3922 unsigned int * topfp,
3923 unsigned int * topgp,
3924 unsigned int * tophp)
3926 register DdNode *F, *G, *H, *r, *f, *g, *h;
3927 register unsigned int topf, topg, toph;
3944 if ((topf > toph) || (topf == toph && f > h)) {
3954 }
else if (H == one) {
3955 if ((topf > topg) || (topf == topg && f > g)) {
3966 if ((topf > topg) || (topf == topg && f > g)) {
4024 unsigned int * topfp,
4025 unsigned int * topgp,
4026 unsigned int * tophp)
4028 register DdNode *r, *f, *g, *h;
4139 #ifdef DD_CACHE_PROFILE 4140 #define DD_HYSTO_BINS 8 4200 unsigned int cacheSize ,
4201 unsigned int maxCacheSize )
4204 unsigned int logSize;
4205 #ifndef DD_CACHE_PROFILE 4213 cacheSize = 1 << logSize;
4215 if (unique->
acache == NULL) {
4222 #ifdef DD_CACHE_PROFILE 4234 unique->
cacheShift =
sizeof(int) * 8 - logSize;
4239 2 * (int) cacheSize;
4255 for (i = 0; (unsigned) i < cacheSize; i++) {
4258 #ifdef DD_CACHE_PROFILE 4259 unique->
cache[i].count = 0;
4295 uf = (
ptruint) f | (op & 0xe);
4300 entry = &table->
cache[posn];
4309 #ifdef DD_CACHE_PROFILE 4340 entry = &table->
cache[posn];
4342 if (entry->
data != NULL) {
4351 #ifdef DD_CACHE_PROFILE 4381 entry = &table->
cache[posn];
4383 if (entry->
data != NULL) {
4392 #ifdef DD_CACHE_PROFILE 4425 uf = (
ptruint) f | (op & 0xe);
4429 cache = table->
cache;
4431 if (cache == NULL) {
4442 if (data->
ref == 0) {
4487 uf = (
ptruint) f | (op & 0xe);
4491 cache = table->
cache;
4493 if (cache == NULL) {
4504 if (data->
ref == 0) {
4547 cache = table->
cache;
4549 if (cache == NULL) {
4556 if (en->
data != NULL && en->
f==f && en->
g==g && en->
h==(
ptruint)op) {
4559 if (data->
ref == 0) {
4600 cache = table->
cache;
4602 if (cache == NULL) {
4612 if (data->
ref == 0) {
4655 cache = table->
cache;
4657 if (cache == NULL) {
4664 if (en->
data != NULL && en->
f==f && en->
g==g && en->
h==(
ptruint)op) {
4667 if (data->
ref == 0) {
4708 cache = table->
cache;
4710 if (cache == NULL) {
4720 if (data->
ref == 0) {
4767 uf = (
ptruint) f | (op & 0xe);
4771 cache = table->
cache;
4773 if (cache == NULL) {
4783 if (en->
data != NULL &&
4825 #ifdef DD_CACHE_PROFILE 4826 double count, mean, meansq, stddev, expected;
4829 double *hystogramQ, *hystogramR;
4830 int nbins = DD_HYSTO_BINS;
4833 double totalcount, exStddev;
4835 meansq = mean = expected = 0.0;
4836 max = min = (long) cache[0].count;
4840 hystogramQ =
ALLOC(
double, nbins);
4841 if (hystogramQ == NULL) {
4845 hystogramR =
ALLOC(
double, nbins);
4846 if (hystogramR == NULL) {
4851 for (i = 0; i < nbins; i++) {
4856 for (i = 0; i < slots; i++) {
4857 thiscount = (long) cache[i].count;
4858 if (thiscount > max) {
4862 if (thiscount < min) {
4866 if (thiscount == 0) {
4869 count = (double) thiscount;
4871 meansq += count * count;
4872 totalcount += count;
4873 expected += count * (double) i;
4874 bin = (i * nbins) / slots;
4875 hystogramQ[bin] += (double) thiscount;
4877 hystogramR[bin] += (double) thiscount;
4879 mean /= (double) slots;
4880 meansq /= (double) slots;
4884 stddev = sqrt(meansq - mean*mean);
4885 exStddev = sqrt((1 - 1/(
double) slots) * totalcount / (
double) slots);
4887 retval = fprintf(fp,
"Cache average accesses = %g\n", mean);
4888 if (retval == EOF)
return(0);
4889 retval = fprintf(fp,
"Cache access standard deviation = %g ", stddev);
4890 if (retval == EOF)
return(0);
4891 retval = fprintf(fp,
"(expected = %g)\n", exStddev);
4892 if (retval == EOF)
return(0);
4893 retval = fprintf(fp,
"Cache max accesses = %ld for slot %d\n", max, imax);
4894 if (retval == EOF)
return(0);
4895 retval = fprintf(fp,
"Cache min accesses = %ld for slot %d\n", min, imin);
4896 if (retval == EOF)
return(0);
4897 exUsed = 100.0 * (1.0 - exp(-totalcount / (
double) slots));
4898 retval = fprintf(fp,
"Cache used slots = %.2f%% (expected %.2f%%)\n",
4899 100.0 - (
double) nzeroes * 100.0 / (
double) slots,
4901 if (retval == EOF)
return(0);
4903 if (totalcount > 0) {
4904 expected /= totalcount;
4905 retval = fprintf(fp,
"Cache access hystogram for %d bins", nbins);
4906 if (retval == EOF)
return(0);
4907 retval = fprintf(fp,
" (expected bin value = %g)\nBy quotient:",
4909 if (retval == EOF)
return(0);
4910 for (i = nbins - 1; i>=0; i--) {
4911 retval = fprintf(fp,
" %.0f", hystogramQ[i]);
4912 if (retval == EOF)
return(0);
4914 retval = fprintf(fp,
"\nBy residue: ");
4915 if (retval == EOF)
return(0);
4916 for (i = nbins - 1; i>=0; i--) {
4917 retval = fprintf(fp,
" %.0f", hystogramR[i]);
4918 if (retval == EOF)
return(0);
4920 retval = fprintf(fp,
"\n");
4921 if (retval == EOF)
return(0);
4927 for (i = 0; i < slots; i++) {
4928 nzeroes += cache[i].
h == 0;
4933 retval = fprintf(fp,
"Cache used slots = %.2f%% (expected %.2f%%)\n",
4934 100.0 - (
double) nzeroes * 100.0 / (
double) slots,
4936 if (retval == EOF)
return(0);
4961 unsigned int slots, oldslots;
4966 #ifndef DD_CACHE_PROFILE 4971 oldcache = table->
cache;
4972 oldacache = table->
acache;
4977 (void) fprintf(table->
err,
"Resizing the cache from %d to %d entries\n",
4979 (void) fprintf(table->
err,
4980 "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
4988 MMoutOfMemory = saveHandler;
4990 if (cache == NULL) {
4992 (void) fprintf(table->
err,
"Resizing failed. Giving up.\n");
4995 table->
acache = oldacache;
5004 #ifdef DD_CACHE_PROFILE 5005 table->
cache = cache;
5018 for (i = 0; (unsigned) i < slots; i++) {
5019 cache[i].
data = NULL;
5021 #ifdef DD_CACHE_PROFILE 5027 for (i = 0; (unsigned) i < oldslots; i++) {
5029 if (old->
data != NULL) {
5031 entry = &cache[posn];
5036 #ifdef DD_CACHE_PROFILE 5048 offset = (double) (
int) (slots * table->
minHit + 1);
5077 cache = table->
cache;
5078 for (i = 0; i < slots; i++) {
5080 cache[i].
data = NULL;
5276 for (i = 0; i < (unsigned) table->
size; i++) {
5278 if (i != (
unsigned) table->
perm[index]) {
5279 (void) fprintf(table->
err,
5280 "Permutation corrupted: invperm[%u] = %d\t perm[%d] = %d\n",
5281 i, index, index, table->
perm[index]);
5289 for (j = 0; j < slots; j++) {
5291 while (f != sentinel) {
5294 if ((
int) f->
index != index) {
5295 (void) fprintf(table->
err,
5296 "Error: node has illegal index\n");
5300 if ((
unsigned)
cuddI(table,
cuddT(f)->index) <= i ||
5303 (void) fprintf(table->
err,
5304 "Error: node has illegal children\n");
5309 (void) fprintf(table->
err,
5310 "Error: node has illegal form\n");
5315 (void) fprintf(table->
err,
5316 "Error: node has identical children\n");
5321 (void) fprintf(table->
err,
5322 "Error: live node has dead children\n");
5327 (void) fprintf(table->
err,
"Error: misplaced node\n");
5359 }
else if (
cuddT(f) != NULL &&
cuddE(f) != NULL && f->
ref == 0) {
5362 debugCheckParent(table,f);
5366 "Error: node has illegal Then or Else pointers\n");
5376 fprintf(table->
err,
"Error: wrong number of total nodes\n");
5380 fprintf(table->
err,
"Error: wrong number of dead nodes\n");
5386 for (i = 0; i < (unsigned) table->
sizeZ; i++) {
5388 if (i != (
unsigned) table->
permZ[index]) {
5389 (void) fprintf(table->
err,
5390 "Permutation corrupted: invpermZ[%u] = %d\t permZ[%d] = %d in ZDD\n",
5391 i, index, index, table->
permZ[index]);
5398 for (j = 0; j < slots; j++) {
5403 if ((
int) f->
index != index) {
5404 (void) fprintf(table->
err,
5405 "Error: ZDD node has illegal index\n");
5411 (void) fprintf(table->
err,
5412 "Error: ZDD node has complemented children\n");
5416 if ((
unsigned)
cuddIZ(table,
cuddT(f)->index) <= i ||
5418 (void) fprintf(table->
err,
5419 "Error: ZDD node has illegal children\n");
5426 (void) fprintf(table->
err,
5427 "Error: ZDD node has zero then child\n");
5431 if (
cuddT(f)->ref == 0 ||
cuddE(f)->ref == 0) {
5432 (void) fprintf(table->
err,
5433 "Error: ZDD live node has dead children\n");
5465 }
else if (
cuddT(f) != NULL &&
cuddE(f) != NULL && f->
ref == 0) {
5468 debugCheckParent(table,f);
5472 "Error: ZDD node has illegal Then or Else pointers\n");
5483 "Error: wrong number of total nodes in ZDD\n");
5488 "Error: wrong number of dead nodes in ZDD\n");
5499 for (j = 0; j < slots; j++) {
5505 fprintf(table->
err,
"Error: node has illegal index\n");
5506 #if SIZEOF_VOID_P == 8 5508 " node 0x%lx, id = %u, ref = %u, value = %g\n",
5512 " node 0x%x, id = %hu, ref = %hu, value = %g\n",
5524 (void) fprintf(table->
err,
5525 "Error: wrong number of total nodes in constants\n");
5529 (void) fprintf(table->
err,
5530 "Error: wrong number of dead nodes in constants\n");
5534 while (
st_gen(gen, &f, &count)) {
5536 #if SIZEOF_VOID_P == 8 5537 fprintf(table->
err,
"ref count error at node 0x%lx, count = %d, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",(
ptruint)f,count,f->
index,f->ref,(
ptruint)
cuddT(f),(
ptruint)
cuddE(f));
5539 fprintf(table->
err,
"ref count error at node 0x%x, count = %d, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",(
ptruint)f,count,f->index,f->ref,(
ptruint)
cuddT(f),(
ptruint)
cuddE(f));
5599 for (i = 0; i < size; i++) {
5602 keys = subtable->
keys;
5603 dead = subtable->
dead;
5605 slots = subtable->
slots;
5606 shift = subtable->
shift;
5607 logSlots =
sizeof(int) * 8 - shift;
5608 if (((slots >> logSlots) << logSlots) != slots) {
5609 (void) fprintf(table->
err,
5610 "Unique table %d is not the right power of 2\n", i);
5611 (void) fprintf(table->
err,
5612 " slots = %u shift = %d\n", slots, shift);
5614 totalSlots += slots;
5616 for (j = 0; (unsigned) j < slots; j++) {
5618 if (node != sentinel) {
5621 while (node != sentinel) {
5623 if (node->
ref == 0) {
5630 (void) fprintf(table->
err,
"Wrong number of keys found \ 5631 in unique table %d (difference=%d)\n", i, keys);
5635 (void) fprintf(table->
err,
"Wrong number of dead found \ 5636 in unique table no. %d (difference=%d)\n", i, dead);
5641 size = table->
sizeZ;
5643 for (i = 0; i < size; i++) {
5646 keys = subtable->
keys;
5647 dead = subtable->
dead;
5649 totalSlots += subtable->
slots;
5651 for (j = 0; (unsigned) j < subtable->slots; j++) {
5656 while (node != NULL) {
5658 if (node->
ref == 0) {
5665 (void) fprintf(table->
err,
"Wrong number of keys found \ 5666 in ZDD unique table no. %d (difference=%d)\n", i, keys);
5670 (void) fprintf(table->
err,
"Wrong number of dead found \ 5671 in ZDD unique table no. %d (difference=%d)\n", i, dead);
5678 keys = subtable->
keys;
5679 dead = subtable->
dead;
5681 totalSlots += subtable->
slots;
5683 for (j = 0; (unsigned) j < subtable->slots; j++) {
5688 while (node != NULL) {
5690 if (node->
ref == 0) {
5697 (void) fprintf(table->
err,
"Wrong number of keys found \ 5698 in the constant table (difference=%d)\n", keys);
5702 (void) fprintf(table->
err,
"Wrong number of dead found \ 5703 in the constant table (difference=%d)\n", dead);
5705 if ((
unsigned) totalKeys != table->
keys + table->
keysZ) {
5706 (void) fprintf(table->
err,
"Wrong number of total keys found \ 5707 (difference=%d)\n", (
int) (totalKeys-table->
keys));
5709 if ((
unsigned) totalSlots != table->
slots) {
5710 (void) fprintf(table->
err,
"Wrong number of total slots found \ 5711 (difference=%d)\n", (
int) (totalSlots-table->
slots));
5714 (void) fprintf(table->
err,
"Wrong number of minimum dead found \ 5715 (%u vs. %u)\n", table->
minDead,
5716 (
unsigned) (table->
gcFrac * (double) table->
slots));
5718 if ((
unsigned) totalDead != table->
dead + table->
deadZ) {
5719 (void) fprintf(table->
err,
"Wrong number of total dead found \ 5720 (difference=%d)\n", (
int) (totalDead-table->
dead));
5722 (void) fprintf(table->
out,
"Average length of non-empty lists = %g\n",
5723 (
double) table->
keys / (double) nonEmpty);
5761 int ntables = dd->
size;
5771 #if SIZEOF_VOID_P == 8 5772 retval = fprintf(dd->
out,
"*** DD heap profile for 0x%lx ***\n",
5775 retval = fprintf(dd->out,
"*** DD heap profile for 0x%x ***\n",
5778 if (retval == EOF)
return 0;
5781 for (i=0; i<ntables; i++) {
5782 nodes = subtables[i].
keys - subtables[i].
dead;
5785 retval = fprintf(dd->out,
"%5d: %5d nodes\n", i, nodes);
5786 if (retval == EOF)
return 0;
5787 if (nodes > maxnodes) {
5794 nodes = dd->constants.keys - dd->constants.dead;
5797 retval = fprintf(dd->out,
"const: %5d nodes\n", nodes);
5798 if (retval == EOF)
return 0;
5799 if (nodes > maxnodes) {
5806 retval = fprintf(dd->out,
"Summary: %d tables, %d non-empty, largest: %d ",
5807 ntables+1, nonempty, largest);
5808 if (retval == EOF)
return 0;
5809 retval = fprintf(dd->out,
"(with %d nodes)\n", maxnodes);
5810 if (retval == EOF)
return 0;
5834 #if SIZEOF_VOID_P == 8 5835 (void) fprintf(fp,
" node 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",(
ptruint)f,f->
index,f->
ref,(
ptruint)
cuddT(f),(
ptruint)
cuddE(f));
5837 (void) fprintf(fp,
" node 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",(
ptruint)f,f->
index,f->
ref,(
ptruint)
cuddT(f),(
ptruint)
cuddE(f));
5883 if (!silent) (void) printf(
"(%d",level);
5885 if (!silent) (void) printf(
",");
5888 while (node != NULL) {
5896 (void) printf(
"%d", (
int) (level + root->
size - 1));
5904 if (root->
parent == NULL) (void) printf(
"\n");
5938 for (i = 0; i <
cuddI(table,node->
index); i++) {
5942 for (j=0;j<slots;j++) {
5946 #if SIZEOF_VOID_P == 8 5947 (void) fprintf(table->
out,
"parent is at 0x%lx, id = %u, ref = %u, then = 0x%lx, else = 0x%lx\n",
5950 (void) fprintf(table->
out,
"parent is at 0x%x, id = %hu, ref = %hu, then = 0x%x, else = 0x%x\n",
5984 for (i = 0; i <
cuddI(table,node->
index); i++) {
5988 for (j=0;j<slots;j++) {
5992 (void) fprintf(table->
err,
5993 "error with zero ref count\n");
5994 (void) fprintf(table->
err,
"parent is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",f,f->
index,f->
ref,
cuddT(f),
cuddE(f));
5995 (void) fprintf(table->
err,
"child is 0x%x, id = %u, ref = %u, then = 0x%x, else = 0x%x\n",node,node->
index,node->
ref,
cuddT(node),
cuddE(node));
6127 if (g == zero || g ==
DD_ZERO(dd)) {
6128 (void) fprintf(dd->
err,
"Cudd_Cofactor: Invalid restriction 1\n");
6162 if (g == one)
return(1);
6231 DdNode *
one,*
zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;
6232 unsigned int topf,topg;
6245 if (g == one)
return(f);
6277 if (g0 == zero || g0 ==
DD_ZERO(dd)) {
6279 }
else if (g1 == zero || g1 ==
DD_ZERO(dd)) {
6282 (void) fprintf(dd->
out,
6283 "Cudd_Cofactor: Invalid restriction 2\n");
6287 if (r == NULL)
return(NULL);
6290 if (t == NULL)
return(NULL);
6420 static int ddTotalShuffles;
6480 int maxBinomial, oldSubsets, newSubsets;
6483 int unused, nvars, level,
result;
6484 int upperBound, lowerBound, cost;
6490 int *newCost = NULL;
6491 int *oldCost = NULL;
6510 if (lower == upper)
return(1);
6515 if (result == 0)
goto cuddExactOutOfMem;
6518 (void) fprintf(table->
out,
"\n");
6519 ddTotalShuffles = 0;
6524 nvars = table->
size;
6525 size = upper - lower + 1;
6529 for (i = lower + 1; i < upper; i++) {
6537 if (maxBinomial == -1)
goto cuddExactOutOfMem;
6539 newOrder =
getMatrix(maxBinomial, size);
6540 if (newOrder == NULL)
goto cuddExactOutOfMem;
6542 newCost =
ALLOC(
int, maxBinomial);
6543 if (newCost == NULL)
goto cuddExactOutOfMem;
6545 oldOrder =
getMatrix(maxBinomial, size);
6546 if (oldOrder == NULL)
goto cuddExactOutOfMem;
6548 oldCost =
ALLOC(
int, maxBinomial);
6549 if (oldCost == NULL)
goto cuddExactOutOfMem;
6552 if (bestOrder == NULL)
goto cuddExactOutOfMem;
6554 mask =
ALLOC(
char, nvars);
6555 if (mask == NULL)
goto cuddExactOutOfMem;
6558 if (symmInfo == NULL)
goto cuddExactOutOfMem;
6568 for (i = 0; i < size; i++) {
6572 for (i = upper + 1; i < nvars; i++)
6574 oldCost[0] = subsetCost;
6579 for (k = 1; k <= size; k++) {
6581 (void) fprintf(table->
out,
"Processing subsets of size %d\n", k);
6587 for (i = 0; i < oldSubsets; i++) {
6588 order = oldOrder[i];
6590 lowerBound =
computeLB(table, order, roots, cost, lower, upper,
6592 if (lowerBound >= upperBound)
6595 result =
ddShuffle(table, order, lower, upper);
6596 if (result == 0)
goto cuddExactOutOfMem;
6597 upperBound =
updateUB(table,upperBound,bestOrder,lower,upper);
6599 for (j = level; j >= 0; j--) {
6604 subsetCost = cost +
getLevelKeys(table, lower + level);
6605 newSubsets =
updateEntry(table, order, level, subsetCost,
6606 newOrder, newCost, newSubsets, mask,
6614 result =
ddShuffle(table, order, lower, upper);
6615 if (result == 0)
goto cuddExactOutOfMem;
6616 upperBound =
updateUB(table,upperBound,bestOrder,lower,upper);
6621 tmpOrder = oldOrder; tmpCost = oldCost;
6622 oldOrder = newOrder; oldCost = newCost;
6623 newOrder = tmpOrder; newCost = tmpCost;
6625 ddTotalSubsets += newSubsets;
6627 oldSubsets = newSubsets;
6629 result =
ddShuffle(table, bestOrder, lower, upper);
6630 if (result == 0)
goto cuddExactOutOfMem;
6633 (void) fprintf(table->
out,
"\n");
6635 (void) fprintf(table->
out,
"#:S_EXACT %8d: total subsets\n",
6637 (void) fprintf(table->
out,
"#:H_EXACT %8d: total shuffles",
6654 if (bestOrder != NULL)
FREE(bestOrder);
6655 if (oldCost != NULL)
FREE(oldCost);
6656 if (newCost != NULL)
FREE(newCost);
6657 if (symmInfo != NULL)
FREE(symmInfo);
6658 if (mask != NULL)
FREE(mask);
6689 if (n < 0 || n > 33)
return(-1);
6690 if (n < 2)
return(1);
6692 for (result = (
double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
6697 return((
int)result);
6725 if (x == 0)
return(y);
6726 if (y == 0)
return(x);
6728 a = x; b = y; lsbMask = 1;
6779 if (cols*rows == 0)
return(NULL);
6781 if (matrix == NULL)
return(NULL);
6783 if (matrix[0] == NULL) {
6787 for (i = 1; i < rows; i++) {
6788 matrix[i] = matrix[i-1] + cols;
6838 isolated = table->
vars[x]->
ref == 1;
6876 unsigned long localTime;
6890 numvars = table->
size;
6892 (void) fprintf(table->
out,
"%d:", ddTotalShuffles);
6893 for (level = 0; level <
numvars; level++) {
6894 (void) fprintf(table->
out,
" %d", table->
invperm[level]);
6896 (void) fprintf(table->
out,
"\n");
6899 for (level = 0; level <= upper - lower; level++) {
6900 index = permutation[level];
6901 position = table->
perm[index];
6905 result =
ddSiftUp(table,position,level+lower);
6906 if (!result)
return(0);
6913 if (finalSize < initialSize) {
6914 (void) fprintf(table->
out,
"-");
6915 }
else if (finalSize > initialSize) {
6916 (void) fprintf(table->
out,
"+");
6918 (void) fprintf(table->
out,
"=");
6920 if ((ddTotalShuffles & 63) == 0) (
void) fprintf(table->
out,
"\n");
6989 if (newBound < oldBound) {
6991 (void) fprintf(table->
out,
"New upper bound = %d\n", newBound);
6994 for (i = lower; i <= upper; i++)
7032 int maxlevel = lower;
7034 for (i = lower; i <= upper; i++) {
7037 for (j = 0; j < slots; j++) {
7039 while (f != sentinel) {
7053 if (table->
perm[
cuddT(f)->index] > maxlevel)
7054 maxlevel = table->
perm[
cuddT(f)->index];
7099 for (i = lower; i <= maxlevel; i++) {
7102 for (j = 0; j < slots; j++) {
7104 while (f != sentinel) {
7154 for (i = 0; i < lower; i++) {
7160 for (i = lower; i <= lower+level; i++) {
7162 table->
vars[order[i-lower]]->
ref > 1;
7168 if (lower+level+1 < table->
size) {
7169 if (lower+level < upper)
7170 ref = table->
vars[order[level+1]]->
ref;
7179 lb += lb1 > lb2 ? lb1 : lb2;
7214 int size = upper - lower + 1;
7217 for (i = lower; i <= upper; i++)
7219 for (i = level; i < size; i++)
7223 for (i = 0; i < subsets; i++) {
7225 for (j = level; j < size; j++) {
7226 if (mask[subset[j]] == 0)
7232 if (i == subsets || cost < costs[i]) {
7233 for (j = 0; j < size; j++)
7234 orders[i][j] = order[j];
7236 subsets += (i == subsets);
7264 for (i = j; i < level; i++) {
7265 order[i] = order[i+1];
7298 int level, index, next, nextindex;
7302 if (symmInfo == NULL)
return(NULL);
7304 for (level = lower; level <= upper; level++) {
7305 index = table->
invperm[level];
7307 nextindex = table->
invperm[next];
7308 symmInfo[index] = nextindex;
7337 i = symmInfo[index];
7338 while (i != index) {
7339 if (index < i && table->perm[i] <= level)
7476 #define STOREDD(i,j) storedd[(i)*(numvars+1)+(j)] 7493 static int array_hash (
char *array,
int modulus);
7494 static int array_compare (
const char *array1,
const char *array2);
7497 static double find_average_fitness (
void);
7499 static int PMX (
int maxvar);
7500 static int roulette (
int *p1,
int *p2);
7541 double average_fitness;
7581 for (i = 0; i <
popsize; i++) {
7585 if (computed == NULL) {
7593 for (i = 0; i <
numvars; i++) {
7608 for (i = 0; i <
numvars; i++) {
7624 for (i = 1; i <
popsize; i++) {
7649 (void) fprintf(table->
out,
"Initial population after sifting\n");
7650 for (m = 0; m <
popsize; m++) {
7651 for (i = 0; i <
numvars; i++) {
7652 (void) fprintf(table->
out,
" %2d",
STOREDD(m,i));
7654 (void) fprintf(table->
out,
" : %3d (%d)\n",
7662 average_fitness = find_average_fitness();
7663 (void) fprintf(table->
out,
"\nInitial population: best fitness = %d, average fitness %8.3f",
STOREDD(small,numvars),average_fitness);
7675 if (
cross >= popsize) {
7680 for (m = 0; m <
cross; m++) {
7691 for (i = popsize; i <= popsize+1; i++) {
7719 if (
repeat[index] == 0) {
7720 int *pointer = &
STOREDD(index,0);
7733 for (n = 0; n <=
numvars; n++) {
7760 average_fitness = find_average_fitness();
7761 (void) fprintf(table->
out,
"\nFinal population: best fitness = %d, average fitness %8.3f",
STOREDD(small,numvars),average_fitness);
7808 (void) fprintf(table->
out,
"Initial population before sifting\n");
7809 for (i = 0; i < 2; i++) {
7810 for (j = 0; j <
numvars; j++) {
7811 (void) fprintf(table->
out,
" %2d",
STOREDD(i,j));
7813 (void) fprintf(table->
out,
"\n");
7817 for (i = 2; i <
popsize; i++) {
7818 for (j = 0; j <
numvars; j++) {
7824 for (j = 0; j <
numvars; j++) {
7827 }
while (used[next] != 0);
7834 for (j = 0; j <
numvars; j++) {
7835 (void) fprintf(table->
out,
" %2d",
STOREDD(i,j));
7837 (void) fprintf(table->
out,
"\n");
7870 while (y >= x_low) {
7915 (void) fprintf(table->
out,
"\nCache hit for index %d", index);
7928 for (j = 0; j <
numvars; j++) {
7930 position = table->
perm[i];
7934 if (size > limit)
break;
7939 (void) fprintf(table->
out,
"\n");
7945 for (j = 0; j <
numvars; j++) {
7974 while (
repeat[big] > 1) big++;
7975 for (i = big + 1; i <
popsize; i++) {
8026 intarray = (
int *) array;
8028 for (i = 0; i <
numvars; i++) {
8029 val = val * 997 + intarray[i];
8032 return ((val < 0) ? -val : val) % modulus;
8051 const char * array1,
8052 const char * array2)
8055 int *intarray1, *intarray2;
8057 intarray1 = (
int *) array1;
8058 intarray2 = (
int *) array2;
8060 for (i = 0; i <
numvars; i++) {
8061 if (intarray1[i] != intarray2[i])
return(1);
8085 for (i = 1; i <
popsize; i++) {
8108 find_average_fitness(
void)
8111 int total_fitness = 0;
8112 double average_fitness;
8114 for (i = 0; i <
popsize; i++) {
8117 average_fitness = (double) total_fitness / (
double)
popsize;
8118 return(average_fitness);
8148 inv1 =
ALLOC(
int,maxvar);
8152 inv2 =
ALLOC(
int,maxvar);
8173 }
while (cut1 == cut2);
8177 (void) fprintf(table->
out,
8178 "Crossover of %d (mom) and %d (dad) between %d and %d\n",
8180 for (i = 0; i <
numvars; i++) {
8181 if (i == cut1 || i == cut2) (void) fprintf(table->
out,
"|");
8182 (void) fprintf(table->
out,
"%2d ",
STOREDD(mom,i));
8184 (void) fprintf(table->
out,
"\n");
8185 for (i = 0; i <
numvars; i++) {
8186 if (i == cut1 || i == cut2) (void) fprintf(table->
out,
"|");
8187 (void) fprintf(table->
out,
"%2d ",
STOREDD(dad,i));
8189 (void) fprintf(table->
out,
"\n");
8193 for (i = 0; i < maxvar; i++) {
8199 for (i = cut1; i != cut2; i = (i == numvars-1) ? 0 : i+1) {
8207 for (i = cut2; i != cut1; i = (i == numvars-1 ) ? 0 : i+1) {
8226 for (i = 0; i <
numvars; i++) {
8227 if (i == cut1 || i == cut2) (void) fprintf(table->
out,
"|");
8230 (void) fprintf(table->
out,
"\n");
8231 for (i = 0; i <
numvars; i++) {
8232 if (i == cut1 || i == cut2) (void) fprintf(table->
out,
"|");
8235 (void) fprintf(table->
out,
"\n");
8267 if (wheel == NULL) {
8274 for (i = 1; i <
popsize; i++) {
8285 for (i = 0; i <
popsize; i++) {
8286 if (spin <= wheel[i])
break;
8294 spin = wheel[popsize-1] * (double)
Cudd_Random() / 2147483561.0;
8295 for (i = 0; i <
popsize; i++) {
8296 if (spin <= wheel[i])
break;
8391 #define DD_NORMAL_SIFT 0 8392 #define DD_LAZY_SIFT 1 8395 #define DD_SIFT_DOWN 0 8396 #define DD_SIFT_UP 1 8425 extern int ddTotalNISwaps;
8426 static int extsymmcalls;
8428 static int secdiffcalls;
8430 static int secdiffmisfire;
8520 tempTree = table->
tree == NULL;
8525 nvars = table->
size;
8528 if (pr > 0 && !tempTree) (void) fprintf(table->
out,
"cuddTreeSifting:");
8539 (void) fprintf(table->
out,
"\n");
8541 (void) fprintf(table->
out,
"#:IM_NODES %8d: group tree nodes\n",
8542 ddCountInternalMtrNodes(table,table->
tree));
8549 for (i = 0; i < nvars; i++)
8560 (void) fprintf(table->
out,
"\nextsymmcalls = %d\n",extsymmcalls);
8561 (void) fprintf(table->
out,
"extsymm = %d",extsymm);
8565 (void) fprintf(table->
out,
"\nsecdiffcalls = %d\n",secdiffcalls);
8566 (void) fprintf(table->
out,
"secdiff = %d\n",secdiff);
8567 (void) fprintf(table->
out,
"secdiffmisfire = %d",secdiffmisfire);
8611 while (auxnode != NULL) {
8612 if (auxnode->
child != NULL) {
8625 }
else if (auxnode->
size > 1) {
8649 ddCountInternalMtrNodes(
8654 int count,nodeCount;
8659 while (auxnode != NULL) {
8662 count = ddCountInternalMtrNodes(table,auxnode->
child);
8697 unsigned int initialSize;
8708 (void) fprintf(table->
out,
" ");
8722 if (initialSize <= table->keys - table->
isolated)
8726 (
void) fprintf(table->
out,
"\n");
8728 }
while (result != 0);
8747 (void) fprintf(table->
err,
8748 "Unknown group ckecking method\n");
8765 (void) fprintf(table->
err,
8766 "Unknown group ckecking method\n");
8770 (void) fprintf(table->
out,
"\n");
8774 if (initialSize <= table->keys - table->
isolated)
8778 (
void) fprintf(table->
out,
"\n");
8780 }
while (result != 0);
8794 result =
cuddGa(table,lower,upper);
8803 if (initialSize <= table->keys - table->
isolated)
8807 (
void) fprintf(table->
out,
"\n");
8809 }
while (result != 0);
8830 if (pr > 0) (void) fprintf(table->
out,
"ddReorderChildren:");
8866 if ((
int) treenode->
low >= table->
size) {
8867 *lower = table->
size;
8872 *lower = low = (
unsigned int) table->
perm[treenode->
index];
8873 high = (
int) (low + treenode->
size - 1);
8875 if (high >= table->
size) {
8884 if (auxnode == NULL) {
8885 *upper = (
unsigned int) table->
size - 1;
8892 while (auxnode != NULL) {
8893 int thisLower = table->
perm[auxnode->
low];
8894 int thisUpper = thisLower + auxnode->
size - 1;
8895 if (thisUpper >= table->
size && thisLower < table->size)
8896 *upper = (
unsigned int) thisLower - 1;
8902 *upper = (
unsigned int) high;
8907 assert(treenode->
size >= *upper - *lower + 1);
8934 return((*ptrX) - (*ptrY));
8972 unsigned previousSize;
8976 nvars = table->
size;
8981 var =
ALLOC(
int,nvars);
8984 goto ddGroupSiftingOutOfMem;
8987 if (
entry == NULL) {
8989 goto ddGroupSiftingOutOfMem;
8991 sifted =
ALLOC(
int,nvars);
8992 if (sifted == NULL) {
8994 goto ddGroupSiftingOutOfMem;
8998 for (i = 0, classes = 0; i < nvars; i++) {
9008 qsort((
void *)var,classes,
sizeof(
int),
9012 for (i = 0; i < nvars; i ++) {
9027 if (sifted[xindex] == 1)
9029 x = table->
perm[xindex];
9048 if (!result)
goto ddGroupSiftingOutOfMem;
9053 x = table->
perm[xindex];
9055 if (x != upper && sifted[table->
invperm[x+1]] == 0 &&
9062 if (x != lower && sifted[table->
invperm[x-1]] == 0 &&
9074 while ((
unsigned) x < table->subtables[x].next)
9078 if (!result)
goto ddGroupSiftingOutOfMem;
9081 (void) fprintf(table->
out,
"_");
9082 }
else if (table->
keys > previousSize + table->
isolated) {
9083 (void) fprintf(table->
out,
"^");
9085 (void) fprintf(table->
out,
"*");
9090 (void) fprintf(table->
out,
"-");
9091 }
else if (table->
keys > previousSize + table->
isolated) {
9092 (void) fprintf(table->
out,
"+");
9094 (void) fprintf(table->
out,
"=");
9101 x = table->
perm[xindex];
9108 }
while (x != xInit);
9111 if (lazyFlag == 0 && dissolve) {
9116 }
while (x != xInit);
9121 if (pr > 0) (void) fprintf(table->
out,
"ddGroupSifting:");
9133 ddGroupSiftingOutOfMem:
9135 if (var != NULL)
FREE(var);
9136 if (sifted != NULL)
FREE(sifted);
9169 while ((
unsigned) gybot < table->subtables[gybot].next)
9213 if (pr > 0) (void) fprintf(table->
out,
9214 "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);
9230 for (y = x; y > xLow; y--) {
9231 if (!checkFunction(table,y-1,y))
9242 for (y = x; y < xHigh; y++) {
9243 if (!checkFunction(table,y,y+1))
9247 while ((
unsigned) topbot < table->subtables[topbot].next) {
9259 while ((
unsigned) x < table->subtables[x].next)
9267 if (x == xHigh)
return(1);
9270 goto ddGroupSiftingAuxOutOfMem;
9279 if (!result)
goto ddGroupSiftingAuxOutOfMem;
9290 goto ddGroupSiftingAuxOutOfMem;
9299 if (!result)
goto ddGroupSiftingAuxOutOfMem;
9301 }
else if (x - xLow > xHigh - x) {
9303 goto ddGroupSiftingAuxOutOfMem;
9310 while ((
unsigned) x < table->subtables[x].next)
9315 assert((
unsigned) x <= table->subtables[x].next);
9319 goto ddGroupSiftingAuxOutOfMem;
9327 if (!result)
goto ddGroupSiftingAuxOutOfMem;
9334 goto ddGroupSiftingAuxOutOfMem;
9340 while ((
unsigned) x < table->subtables[x].next)
9348 goto ddGroupSiftingAuxOutOfMem;
9356 if (!result)
goto ddGroupSiftingAuxOutOfMem;
9359 while (moves != NULL) {
9367 ddGroupSiftingAuxOutOfMem:
9368 while (moves != NULL) {
9430 while ((
unsigned) gybot < table->subtables[gybot].next)
9432 for (z = xLow + 1; z <= gybot; z++) {
9435 isolated = table->
vars[zindex]->
ref == 1;
9441 while (x >= xLow && L <= limitSize) {
9444 while ((
unsigned) gybot < table->subtables[gybot].next)
9447 for (z = xLow + 1; z <= gybot; z++) {
9450 isolated = table->
vars[zindex]->
ref == 1;
9454 if (pr > 0 && L != checkL) {
9455 (void) fprintf(table->
out,
9456 "Inaccurate lower bound: L = %d checkL = %d\n",
9461 if (checkFunction(table,x,y)) {
9469 if (move == NULL)
goto ddGroupSiftingUpOutOfMem;
9474 move->
next = *moves;
9485 if (size == 0)
goto ddGroupSiftingUpOutOfMem;
9488 isolated = table->
vars[xindex]->
ref == 1;
9492 if (move == NULL)
goto ddGroupSiftingUpOutOfMem;
9497 move->
next = *moves;
9501 if (pr > 0) (void) fprintf(table->
out,
9502 "ddGroupSiftingUp (2 single groups):\n");
9504 if ((
double) size > (double) limitSize * table->
maxGrowth)
9506 if (size < limitSize) limitSize = size;
9509 if (size == 0)
goto ddGroupSiftingUpOutOfMem;
9515 isolated = table->
vars[zindex]->
ref == 1;
9519 }
while (z != (
int) (*moves)->y);
9520 if ((
double) size > (
double) limitSize * table->
maxGrowth)
9522 if (size < limitSize) limitSize = size;
9530 ddGroupSiftingUpOutOfMem:
9531 while (*moves != NULL) {
9532 move = (*moves)->
next;
9567 int isolated, allVars;
9596 for (z = xHigh; z > gxtop; z--) {
9599 isolated = table->
vars[zindex]->
ref == 1;
9605 while (y <= xHigh && size - R < limitSize) {
9609 for (z = xHigh; z > gxtop; z--) {
9612 isolated = table->
vars[zindex]->
ref == 1;
9623 if (checkFunction(table,x,y)) {
9629 if (move == NULL)
goto ddGroupSiftingDownOutOfMem;
9634 move->
next = *moves;
9642 isolated = table->
vars[yindex]->
ref == 1;
9650 if (size == 0)
goto ddGroupSiftingDownOutOfMem;
9654 if (move == NULL)
goto ddGroupSiftingDownOutOfMem;
9659 move->
next = *moves;
9663 if (pr > 0) (void) fprintf(table->
out,
9664 "ddGroupSiftingDown (2 single groups):\n");
9666 if ((
double) size > (double) limitSize * table->
maxGrowth)
9668 if (size < limitSize) limitSize = size;
9679 isolated = table->
vars[zindex]->
ref == 1;
9683 }
while (z <= gybot);
9685 if (size == 0)
goto ddGroupSiftingDownOutOfMem;
9686 if ((
double) size > (
double) limitSize * table->
maxGrowth)
9688 if (size < limitSize) limitSize = size;
9692 for (z = gxtop + 1; z <= gybot; z++) {
9695 isolated = table->
vars[zindex]->
ref == 1;
9706 ddGroupSiftingDownOutOfMem:
9707 while (*moves != NULL) {
9708 move = (*moves)->
next;
9737 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
9739 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 9740 int initialSize,bestSize;
9750 xsize = xbot - xtop + 1;
9752 while ((
unsigned) ybot < table->subtables[ybot].next)
9755 ysize = ybot - ytop + 1;
9757 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 9758 initialSize = bestSize = table->
keys - table->
isolated;
9761 for (i = 1; i <= ysize; i++) {
9762 for (j = 1; j <= xsize; j++) {
9764 if (size == 0)
goto ddGroupMoveOutOfMem;
9765 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 9766 if (size < bestSize)
9769 swapx = x; swapy = y;
9776 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 9777 if ((bestSize < initialSize) && (bestSize < size))
9778 (void) fprintf(table->
out,
"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size);
9783 for (i = 0; i < ysize - 1; i++) {
9791 for (i = 0; i < xsize - 1; i++) {
9798 if (pr > 0) (void) fprintf(table->
out,
"ddGroupMove:\n");
9803 if (move == NULL)
goto ddGroupMoveOutOfMem;
9808 move->
next = *moves;
9813 ddGroupMoveOutOfMem:
9814 while (*moves != NULL) {
9815 move = (*moves)->
next;
9841 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
9852 xsize = xbot - xtop + 1;
9854 while ((
unsigned) ybot < table->subtables[ybot].next)
9857 ysize = ybot - ytop + 1;
9860 for (i = 1; i <= ysize; i++) {
9861 for (j = 1; j <= xsize; j++) {
9874 for (i = 0; i < ysize - 1; i++) {
9882 for (i = 0; i < xsize - 1; i++) {
9889 if (pr > 0) (void) fprintf(table->
out,
"ddGroupMoveBackward:\n");
9921 unsigned int pairlev;
9928 for (move = moves; move != NULL; move = move->
next) {
9929 if (move->
size < size) {
9932 }
else if (move->
size == size) {
9933 if (end_move == NULL) end_move = move;
9939 if (moves != NULL) {
9941 index = (upFlag == 1) ?
9946 for (move = moves; move != NULL; move = move->
next) {
9947 if (move->
size == size) {
9949 tmp_diff = (move->
x > pairlev) ?
9950 move->
x - pairlev : pairlev - move->
x;
9952 tmp_diff = (move->
y > pairlev) ?
9953 move->
y - pairlev : pairlev - move->
y;
9955 if (tmp_diff < diff) {
9964 for (move = moves; move != NULL; move = move->
next) {
9965 if (move->
size < size) {
9974 for (move = moves; move != NULL; move = move->
next) {
9976 if (move == end_move)
return(1);
9978 if (move->
size == size)
return(1);
9983 if (!res)
return(0);
9985 if (pr > 0) (void) fprintf(table->
out,
"ddGroupSiftingBackward:\n");
9994 if (!res)
return(0);
10030 if (treenode != table->
tree) {
10031 for (i = low; i < high; i++)
10038 saveindex = treenode->
index;
10039 newindex = table->
invperm[low];
10040 auxnode = treenode;
10042 auxnode->
index = newindex;
10043 if (auxnode->
parent == NULL ||
10046 auxnode = auxnode->
parent;
10074 while ((
unsigned) boty < table->subtables[boty].next)
10132 if (x==0)
return(0);
10141 threshold = table->
recomb / 100.0;
10142 if (Sx < threshold) {
10146 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 10147 (void) fprintf(table->
out,
10148 "Second difference for %d = %g Pos(%d)\n",
10184 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
10234 for (i = 0; i < slots; i++) {
10236 while (f != sentinel) {
10241 notproj = f1 != one || f0 != one || f->
ref != (
DdHalfWord) 1;
10242 if (f1->
index == (
unsigned) yindex) {
10246 if ((
int) f0->
index != yindex) {
10258 if ((
int) f0->
index == yindex) {
10274 if (f01 != f10 && f11 != f00) {
10286 TotalRefCount = -1;
10289 for (i = 0; i < slots; i++) {
10291 while (f != sentinel) {
10292 TotalRefCount += f->
ref;
10299 res = arccount >= TotalRefCount - arccounter;
10301 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 10303 (void) fprintf(table->
out,
10304 "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
10305 xindex,yindex,x,y);
10334 int xindex = table->
invperm[x];
10335 int yindex = table->
invperm[y];
10373 if (index >= dd->
size || index < 0)
return(0);
10397 if (index >= dd->
size || index < 0)
return(0);
10421 if (index >= dd->
size || index < 0)
return(-1);
10545 unsigned int numVars ,
10546 unsigned int numVarsZ ,
10547 unsigned int numSlots ,
10548 unsigned int cacheSize ,
10549 unsigned long maxMemory )
10554 unsigned int maxCacheSize;
10555 unsigned int looseUpTo;
10559 if (maxMemory == 0) {
10562 looseUpTo = (
unsigned int) ((maxMemory /
sizeof(
DdNode)) /
10564 unique =
cuddInitTable(numVars,numVarsZ,numSlots,looseUpTo);
10565 if (unique == NULL)
return(NULL);
10566 unique->
maxmem = (
unsigned long) maxMemory / 10 * 9;
10567 maxCacheSize = (
unsigned int) ((maxMemory /
sizeof(
DdCache)) /
10570 if (result == 0)
return(NULL);
10575 MMoutOfMemory = saveHandler;
10576 if (unique->
stash == NULL) {
10577 (void) fprintf(unique->
err,
"Unable to set aside memory\n");
10582 if (unique->
one == NULL)
return(0);
10585 if (unique->
zero == NULL)
return(0);
10587 #ifdef HAVE_IEEE_754 10590 (void) fprintf(unique->
err,
"Warning: Crippled infinite values\n");
10591 (void) fprintf(unique->
err,
"Recompile without -DHAVE_IEEE_754\n");
10607 if (unique->
vars == NULL) {
10611 for (i = 0; i < unique->
size; i++) {
10613 if (unique->
vars[i] == NULL)
return(0);
10675 if (zdd->
univ == NULL) {
10682 for (i = zdd->
sizeZ - 1; i >= 0; i--) {
10683 unsigned int index = zdd->
invpermZ[i];
10693 zdd->
univ[i] = res;
10814 #if SIZEOF_LONG == 8 10887 int posn, word, bit;
10891 assert(y < table->size);
10895 posn = ((((table->
size << 1) - x - 3) * x) >> 1) + y - 1;
10897 bit = posn & (
BPL-1);
10898 table->
interact[word] |= 1L << bit;
10922 int posn, word, bit,
result;
10931 assert(y < table->size);
10935 posn = ((((table->
size << 1) - x - 3) * x) >> 1) + y - 1;
10937 bit = posn & (
BPL-1);
10938 result = (table->
interact[word] >> bit) & 1L;
10967 unsigned long words;
10974 unsigned long n = (
unsigned long) table->
size;
10976 words = ((n * (n-1)) >> (1 +
LOGBPL)) + 1;
10978 if (interact == NULL) {
10982 for (i = 0; i < words; i++) {
10986 support =
ALLOC(
char,n);
10987 if (support == NULL) {
10992 for (i = 0; i < n; i++) {
10996 for (i = 0; i < n; i++) {
10999 for (j = 0; j < slots; j++) {
11001 while (f != sentinel) {
11051 support[f->
index] = 1;
11108 int n = table->
size;
11110 for (i = 0; i < n-1; i++) {
11111 if (support[i] == 1) {
11113 for (j = i+1; j < n; j++) {
11114 if (support[j] == 1) {
11148 for (i = 0; i < table->
size; i++) {
11151 for (j = 0; j < slots; j++) {
11153 while (f != sentinel) {
11244 #define DD_MAX_HASHTABLE_DENSITY 2 11279 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 11280 #define ddLCHash1(f,shift) \ 11281 (((unsigned)(ptruint)(f) * DD_P1) >> (shift)) 11283 #define ddLCHash1(f,shift) \ 11284 (((unsigned)(f) * DD_P1) >> (shift)) 11299 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 11300 #define ddLCHash2(f,g,shift) \ 11301 ((((unsigned)(ptruint)(f) * DD_P1 + \ 11302 (unsigned)(ptruint)(g)) * DD_P2) >> (shift)) 11304 #define ddLCHash2(f,g,shift) \ 11305 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift)) 11320 #define ddLCHash3(f,g,h,shift) ddCHash2(f,g,h,shift) 11366 unsigned int keysize;
11367 unsigned int itemsize;
11368 unsigned int slots;
11373 while (cache != NULL) {
11376 slots = cache->
slots;
11377 item = cache->
item;
11378 for (i = 0; i < slots; i++) {
11379 if (item->
value != NULL) {
11381 item->
value = NULL;
11384 for (j = 0; j < keysize; j++) {
11386 item->
value = NULL;
11394 cache = cache->
next;
11419 while (cache != NULL) {
11421 cache = cache->
next;
11428 #ifdef DD_CACHE_PROFILE 11430 #define DD_HYSTO_BINS 8 11445 cuddLocalCacheProfile(
11448 double count, mean, meansq, stddev, expected;
11451 int i, retval, slots;
11453 int nbins = DD_HYSTO_BINS;
11461 slots = cache->
slots;
11463 meansq = mean = expected = 0.0;
11464 max = min = (long) cache->
item[0].count;
11465 imax = imin = nzeroes = 0;
11468 hystogram =
ALLOC(
long, nbins);
11469 if (hystogram == NULL) {
11472 for (i = 0; i < nbins; i++) {
11476 for (i = 0; i < slots; i++) {
11479 thiscount = (long) entry->count;
11480 if (thiscount > max) {
11484 if (thiscount < min) {
11488 if (thiscount == 0) {
11491 count = (double) thiscount;
11493 meansq += count * count;
11494 totalcount += count;
11495 expected += count * (double) i;
11496 bin = (i * nbins) / slots;
11497 hystogram[bin] += thiscount;
11499 mean /= (double) slots;
11500 meansq /= (double) slots;
11501 stddev = sqrt(meansq - mean*mean);
11503 retval = fprintf(fp,
"Cache stats: slots = %d average = %g ", slots, mean);
11504 if (retval == EOF)
return(0);
11505 retval = fprintf(fp,
"standard deviation = %g\n", stddev);
11506 if (retval == EOF)
return(0);
11507 retval = fprintf(fp,
"Cache max accesses = %ld for slot %d\n", max, imax);
11508 if (retval == EOF)
return(0);
11509 retval = fprintf(fp,
"Cache min accesses = %ld for slot %d\n", min, imin);
11510 if (retval == EOF)
return(0);
11511 retval = fprintf(fp,
"Cache unused slots = %d\n", nzeroes);
11512 if (retval == EOF)
return(0);
11515 expected /= totalcount;
11516 retval = fprintf(fp,
"Cache access hystogram for %d bins", nbins);
11517 if (retval == EOF)
return(0);
11518 retval = fprintf(fp,
" (expected bin value = %g)\n# ", expected);
11519 if (retval == EOF)
return(0);
11520 for (i = nbins - 1; i>=0; i--) {
11521 retval = fprintf(fp,
"%ld ", hystogram[i]);
11522 if (retval == EOF)
return(0);
11524 retval = fprintf(fp,
"\n");
11525 if (retval == EOF)
return(0);
11550 unsigned int keySize,
11551 unsigned int initSize)
11557 if (hash == NULL) {
11568 if (initSize < 2) initSize = 2;
11571 hash->
shift =
sizeof(int) * 8 - logSize;
11573 if (hash->
bucket == NULL) {
11607 for (i = 0; i < numBuckets; i++) {
11608 bucket = hash->
bucket[i];
11609 while (bucket != NULL) {
11611 bucket = bucket->
next;
11616 while (memlist != NULL) {
11647 #pragma pointer_size save 11648 #pragma pointer_size short 11653 while (memlist != NULL) {
11662 #pragma pointer_size restore 11701 if (result == 0)
return(0);
11704 if (item == NULL)
return(0);
11706 item->
value = value;
11708 item->
count = count;
11709 for (i = 0; i < hash->
keysize; i++) {
11710 item->
key[i] = key[i];
11714 hash->
bucket[posn] = item;
11745 unsigned int i, keysize;
11752 item = hash->
bucket[posn];
11756 while (item != NULL) {
11759 for (i = 0; i < keysize; i++) {
11760 if (key[i] != key2[i]) {
11768 if (item->
count == 0) {
11770 if (prev == NULL) {
11819 if (result == 0)
return(0);
11822 if (item == NULL)
return(0);
11824 item->
value = value;
11826 item->
count = count;
11830 hash->
bucket[posn] = item;
11867 item = hash->
bucket[posn];
11870 while (item != NULL) {
11875 if (item->
count == 0) {
11877 if (prev == NULL) {
11925 if (result == 0)
return(0);
11928 if (item == NULL)
return(0);
11935 hash->
bucket[posn] = item;
11969 item = hash->
bucket[posn];
11971 while (item != NULL) {
11972 if (f == item->
key[0]) {
11973 return ((
void *) item->
value);
12013 if (result == 0)
return(0);
12016 if (item == NULL)
return(0);
12018 item->
value = value;
12020 item->
count = count;
12025 hash->
bucket[posn] = item;
12063 item = hash->
bucket[posn];
12066 while (item != NULL) {
12068 if ((f == key[0]) && (g == key[1])) {
12071 if (item->
count == 0) {
12073 if (prev == NULL) {
12124 if (result == 0)
return(0);
12127 if (item == NULL)
return(0);
12129 item->
value = value;
12131 item->
count = count;
12137 hash->
bucket[posn] = item;
12176 item = hash->
bucket[posn];
12179 while (item != NULL) {
12181 if ((f == key[0]) && (g == key[1]) && (h == key[2])) {
12184 if (item->
count == 0) {
12186 if (prev == NULL) {
12228 unsigned int slots, oldslots;
12232 olditem = cache->
item;
12233 oldslots = cache->
slots;
12234 slots = cache->
slots = oldslots << 1;
12238 "Resizing local cache from %d to %d entries\n",
12241 "\thits = %.0f\tlookups = %.0f\thit ratio = %5.3f\n",
12247 cache->
item = item =
12249 MMoutOfMemory = saveHandler;
12251 if (item == NULL) {
12253 (void) fprintf(cache->
manager->
err,
"Resizing failed. Giving up.\n");
12255 cache->
slots = oldslots;
12256 cache->
item = olditem;
12261 shift = --(cache->
shift);
12268 for (i = 0; (unsigned) i < oldslots; i++) {
12270 if (old->
value != NULL) {
12284 cache->
lookUps = (double) (
int) (slots * cache->
minHit + 1);
12303 static unsigned int 12306 unsigned int keysize,
12309 unsigned int val = (
unsigned int) (
ptrint) key[0] *
DD_P2;
12312 for (i = 1; i < keysize; i++) {
12316 return(val >> shift);
12366 while (nextCache != NULL) {
12367 if (nextCache == cache) {
12368 *prevCache = nextCache->
next;
12371 prevCache = &(nextCache->
next);
12372 nextCache = nextCache->
next;
12409 numBuckets = oldNumBuckets << 1;
12413 MMoutOfMemory = saveHandler;
12414 if (buckets == NULL) {
12421 shift = --(hash->
shift);
12425 for (j = 0; j < oldNumBuckets; j++) {
12426 item = oldBuckets[j];
12427 while (item != NULL) {
12430 posn =
ddLCHash2(key[0], key[0], shift);
12431 item->
next = buckets[posn];
12432 buckets[posn] = item;
12436 }
else if (hash->
keysize == 2) {
12437 for (j = 0; j < oldNumBuckets; j++) {
12438 item = oldBuckets[j];
12439 while (item != NULL) {
12442 posn =
ddLCHash2(key[0], key[1], shift);
12443 item->
next = buckets[posn];
12444 buckets[posn] = item;
12448 }
else if (hash->
keysize == 3) {
12449 for (j = 0; j < oldNumBuckets; j++) {
12450 item = oldBuckets[j];
12451 while (item != NULL) {
12454 posn =
ddLCHash3(key[0], key[1], key[2], shift);
12455 item->
next = buckets[posn];
12456 buckets[posn] = item;
12461 for (j = 0; j < oldNumBuckets; j++) {
12462 item = oldBuckets[j];
12463 while (item != NULL) {
12466 item->
next = buckets[posn];
12467 buckets[posn] = item;
12498 unsigned int itemsize = hash->
itemsize;
12507 MMoutOfMemory = saveHandler;
12524 (*MMoutOfMemory)((long)((
DD_MEM_CHUNK + 1) * itemsize));
12533 thisOne = (
DdHashItem *) ((
char *) mem + itemsize);
12536 next = (
DdHashItem *) ((
char *) thisOne + itemsize);
12537 thisOne->
next = next;
12541 thisOne->
next = NULL;
12617 #define CUDD_SWAP_MOVE 0 12618 #define CUDD_LINEAR_TRANSFORM_MOVE 1 12619 #define CUDD_INVERSE_TRANSFORM_MOVE 2 12620 #if SIZEOF_LONG == 8 12648 extern int ddTotalNISwaps;
12649 static int ddTotalNumberLinearTr;
12653 static int zero = 0;
12701 int wordsPerRow = ((nvars - 1) >>
LOGBPL) + 1;
12704 for (i = 0; i < nvars; i++) {
12705 for (j = 0; j < wordsPerRow; j++) {
12706 word = table->
linear[i*wordsPerRow + j];
12707 for (k = 0; k <
BPL; k++) {
12708 retval = fprintf(table->
out,
"%ld",word & 1);
12709 if (retval == 0)
return(0);
12713 retval = fprintf(table->
out,
"\n");
12714 if (retval == 0)
return(0);
12765 ddTotalNumberLinearTr = 0;
12768 size = table->
size;
12772 if (table->
linear == NULL) {
12774 if (result == 0)
goto cuddLinearAndSiftingOutOfMem;
12776 (void) fprintf(table->
out,
"\n");
12778 if (result == 0)
goto cuddLinearAndSiftingOutOfMem;
12782 if (result == 0)
goto cuddLinearAndSiftingOutOfMem;
12784 (void) fprintf(table->
out,
"\n");
12786 if (result == 0)
goto cuddLinearAndSiftingOutOfMem;
12792 if (
entry == NULL) {
12794 goto cuddLinearAndSiftingOutOfMem;
12796 var =
ALLOC(
int,size);
12799 goto cuddLinearAndSiftingOutOfMem;
12802 for (i = 0; i < size; i++) {
12803 x = table->
perm[i];
12812 x = table->
perm[var[i]];
12813 if (x < lower || x > upper)
continue;
12818 if (!result)
goto cuddLinearAndSiftingOutOfMem;
12820 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
12821 (void) fprintf(table->
out,
"-");
12822 }
else if (table->
keys > (
unsigned) previousSize + table->
isolated) {
12823 (void) fprintf(table->
out,
"+");
12824 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keys - table->
isolated, var[i]);
12826 (void) fprintf(table->
out,
"=");
12828 fflush(table->
out);
12839 (void) fprintf(table->
out,
"\n#:L_LINSIFT %8d: linear trans.",
12840 ddTotalNumberLinearTr);
12845 cuddLinearAndSiftingOutOfMem:
12848 if (var != NULL)
FREE(var);
12880 int xindex, yindex;
12881 int xslots, yslots;
12882 int xshift, yshift;
12883 int oldxkeys, oldykeys;
12884 int newxkeys, newykeys;
12885 int comple, newcomplement;
12889 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
12895 int count, idcheck;
12912 ddTotalNumberLinearTr++;
12927 newykeys = oldykeys;
12935 isolated = - ((table->
vars[xindex]->
ref == 1) +
12936 (table->
vars[yindex]->
ref == 1));
12946 for (i = 0; i < xslots; i++) {
12948 if (f == sentinel)
continue;
12949 xlist[i] = sentinel;
12955 while ((next = f->
next) != sentinel) {
12968 table->swapSteps += oldxkeys;
12974 while (f != NULL) {
12981 if ((
int) f1->
index == yindex) {
12992 if ((
int) f0->
index == yindex) {
13009 posn =
ddHash(f11, f00, yshift);
13011 previousP = &(ylist[posn]);
13012 newf1 = *previousP;
13013 while (f11 <
cuddT(newf1)) {
13014 previousP = &(newf1->
next);
13015 newf1 = *previousP;
13017 while (f11 ==
cuddT(newf1) && f00 <
cuddE(newf1)) {
13018 previousP = &(newf1->
next);
13019 newf1 = *previousP;
13021 if (
cuddT(newf1) == f11 &&
cuddE(newf1) == f00) {
13026 goto cuddLinearOutOfMem;
13027 newf1->
index = yindex; newf1->
ref = 1;
13028 cuddT(newf1) = f11;
13029 cuddE(newf1) = f00;
13034 newf1->
next = *previousP;
13035 *previousP = newf1;
13058 if (newcomplement) {
13063 posn =
ddHash(f01, f10, yshift);
13065 previousP = &(ylist[posn]);
13066 newf0 = *previousP;
13067 while (f01 <
cuddT(newf0)) {
13068 previousP = &(newf0->
next);
13069 newf0 = *previousP;
13071 while (f01 ==
cuddT(newf0) && f10 <
cuddE(newf0)) {
13072 previousP = &(newf0->
next);
13073 newf0 = *previousP;
13075 if (
cuddT(newf0) == f01 &&
cuddE(newf0) == f10) {
13080 goto cuddLinearOutOfMem;
13081 newf0->
index = yindex; newf0->
ref = 1;
13082 cuddT(newf0) = f01;
13083 cuddE(newf0) = f10;
13088 newf0->
next = *previousP;
13089 *previousP = newf0;
13094 if (newcomplement) {
13104 posn =
ddHash(newf1, newf0, xshift);
13106 previousP = &(xlist[posn]);
13108 while (newf1 <
cuddT(tmp)) {
13109 previousP = &(tmp->
next);
13112 while (newf1 ==
cuddT(tmp) && newf0 <
cuddE(tmp)) {
13113 previousP = &(tmp->
next);
13116 f->
next = *previousP;
13124 for (i = 0; i < yslots; i++) {
13125 previousP = &(ylist[i]);
13127 while (f != sentinel) {
13138 previousP = &(f->
next);
13142 *previousP = sentinel;
13147 (void) fprintf(table->
out,
"Linearly combining %d and %d\n",x,y);
13151 for (i = 0; i < yslots; i++) {
13153 while (f != sentinel) {
13160 if (count != newykeys) {
13161 fprintf(table->
err,
"Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",oldykeys,newykeys,count);
13164 fprintf(table->
err,
"Error in id's of ylist\twrong id's = %d\n",idcheck);
13167 for (i = 0; i < xslots; i++) {
13169 while (f != sentinel) {
13176 if (count != newxkeys || newxkeys != oldxkeys) {
13177 fprintf(table->
err,
"Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",oldxkeys,newxkeys,count);
13180 fprintf(table->
err,
"Error in id's of xlist\twrong id's = %d\n",idcheck);
13183 isolated += (table->
vars[xindex]->
ref == 1) +
13184 (table->
vars[yindex]->
ref == 1);
13195 table->
keys += newykeys - oldykeys;
13208 cuddLinearOutOfMem:
13209 (void) fprintf(table->
err,
"Error: cuddLinearInPlace out of memory\n");
13234 for (i = 0; i < yindex; i++) {
13243 for (i = yindex+1; i < table->
size; i++) {
13280 nvars = table->
size;
13281 wordsPerRow = ((nvars - 1) >>
LOGBPL) + 1;
13282 words = wordsPerRow * nvars;
13284 if (linear == NULL) {
13288 table->
memused += words *
sizeof(long);
13290 for (i = 0; i < words; i++) linear[i] = 0;
13291 for (i = 0; i < nvars; i++) {
13292 word = wordsPerRow * i + (i >>
LOGBPL);
13294 linear[word] = 1 << bit;
13317 int words,oldWords;
13318 int wordsPerRow,oldWordsPerRow;
13319 int nvars,oldNvars;
13323 long *linear,*oldLinear;
13326 oldWordsPerRow = ((oldNvars - 1) >>
LOGBPL) + 1;
13327 oldWords = oldWordsPerRow * oldNvars;
13328 oldLinear = table->
linear;
13330 nvars = table->
size;
13331 wordsPerRow = ((nvars - 1) >>
LOGBPL) + 1;
13332 words = wordsPerRow * nvars;
13334 if (linear == NULL) {
13338 table->
memused += (words - oldWords) *
sizeof(
long);
13339 for (i = 0; i < words; i++) linear[i] = 0;
13342 for (i = 0; i < oldNvars; i++) {
13343 for (j = 0; j < oldWordsPerRow; j++) {
13344 oldWord = oldWordsPerRow * i + j;
13345 word = wordsPerRow * i + j;
13346 linear[word] = oldLinear[oldWord];
13352 for (i = oldNvars; i < nvars; i++) {
13353 word = wordsPerRow * i + (i >>
LOGBPL);
13355 linear[word] = 1 << bit;
13388 return((*ptrX) - (*ptrY));
13434 if (!result)
goto ddLinearAndSiftingAuxOutOfMem;
13436 }
else if (x == xHigh) {
13442 if (!result)
goto ddLinearAndSiftingAuxOutOfMem;
13444 }
else if ((x - xLow) > (xHigh - x)) {
13450 assert(moveUp == NULL || moveUp->
x == x);
13453 if (moveUp == (
Move *) CUDD_OUT_OF_MEM)
goto ddLinearAndSiftingAuxOutOfMem;
13456 if (!result)
goto ddLinearAndSiftingAuxOutOfMem;
13464 assert(moveDown == NULL || moveDown->
y == x);
13467 if (moveDown == (
Move *) CUDD_OUT_OF_MEM)
goto ddLinearAndSiftingAuxOutOfMem;
13470 if (!result)
goto ddLinearAndSiftingAuxOutOfMem;
13473 while (moveDown != NULL) {
13474 move = moveDown->
next;
13478 while (moveUp != NULL) {
13479 move = moveUp->
next;
13486 ddLinearAndSiftingAuxOutOfMem:
13487 while (moveDown != NULL) {
13488 move = moveDown->
next;
13492 while (moveUp != NULL) {
13493 move = moveUp->
next;
13527 int xindex, yindex;
13546 for (x = xLow + 1; x < y; x++) {
13549 isolated = table->
vars[xindex]->
ref == 1;
13553 isolated = table->
vars[yindex]->
ref == 1;
13557 while (x >= xLow && L <= limitSize) {
13561 for (z = xLow + 1; z < y; z++) {
13564 isolated = table->
vars[zindex]->
ref == 1;
13568 isolated = table->
vars[yindex]->
ref == 1;
13571 (void) fprintf(table->
out,
"checkL(%d) != L(%d)\n",checkL,L);
13575 if (size == 0)
goto ddLinearAndSiftingUpOutOfMem;
13577 if (newsize == 0)
goto ddLinearAndSiftingUpOutOfMem;
13579 if (move == NULL)
goto ddLinearAndSiftingUpOutOfMem;
13582 move->
next = moves;
13585 if (newsize >= size) {
13591 if (newsize == 0)
goto ddLinearAndSiftingUpOutOfMem;
13593 if (newsize != size) {
13594 (void) fprintf(table->
out,
"Change in size after identity transformation! From %d to %d\n",size,newsize);
13605 isolated = table->
vars[xindex]->
ref == 1;
13608 if ((
double) size > (
double) limitSize * table->
maxGrowth)
break;
13609 if (size < limitSize) limitSize = size;
13615 ddLinearAndSiftingUpOutOfMem:
13616 while (moves != NULL) {
13617 move = moves->
next;
13651 int xindex, yindex;
13664 for (y = xHigh; y > x; y--) {
13667 isolated = table->
vars[yindex]->
ref == 1;
13673 while (y <= xHigh && size - R < limitSize) {
13676 for (z = xHigh; z > x; z--) {
13679 isolated = table->
vars[zindex]->
ref == 1;
13684 (void) fprintf(table->
out,
"checkR(%d) != R(%d)\n",checkR,R);
13690 isolated = table->
vars[yindex]->
ref == 1;
13694 if (size == 0)
goto ddLinearAndSiftingDownOutOfMem;
13696 if (newsize == 0)
goto ddLinearAndSiftingDownOutOfMem;
13698 if (move == NULL)
goto ddLinearAndSiftingDownOutOfMem;
13701 move->
next = moves;
13704 if (newsize >= size) {
13710 if (newsize == 0)
goto ddLinearAndSiftingDownOutOfMem;
13711 if (newsize != size) {
13712 (void) fprintf(table->
out,
"Change in size after identity transformation! From %d to %d\n",size,newsize);
13720 if ((
double) size > (
double) limitSize * table->
maxGrowth)
break;
13721 if (size < limitSize) limitSize = size;
13727 ddLinearAndSiftingDownOutOfMem:
13728 while (moves != NULL) {
13729 move = moves->
next;
13760 for (move = moves; move != NULL; move = move->
next) {
13761 if (move->
size < size) {
13766 for (move = moves; move != NULL; move = move->
next) {
13767 if (move->
size == size)
return(1);
13770 if (!res)
return(0);
13773 if (!res)
return(0);
13776 if (!res)
return(0);
13802 Move *invmoves = NULL;
13807 for (move = moves; move != NULL; move = move->
next) {
13809 if (invmove == NULL)
goto ddUndoMovesOutOfMem;
13810 invmove->
x = move->
x;
13811 invmove->
y = move->
y;
13812 invmove->
next = invmoves;
13813 invmoves = invmove;
13817 if (!size)
goto ddUndoMovesOutOfMem;
13821 if (!size)
goto ddUndoMovesOutOfMem;
13823 if (!size)
goto ddUndoMovesOutOfMem;
13826 (void) fprintf(table->
err,
"Unforseen event in ddUndoMoves!\n");
13830 if (!size)
goto ddUndoMovesOutOfMem;
13832 if (!size)
goto ddUndoMovesOutOfMem;
13834 invmove->
size = size;
13839 ddUndoMovesOutOfMem:
13840 while (invmoves != NULL) {
13841 move = invmoves->
next;
13869 int nvars = table->
size;
13870 int wordsPerRow = ((nvars - 1) >>
LOGBPL) + 1;
13871 int xstart = wordsPerRow * x;
13872 int ystart = wordsPerRow * y;
13873 long *linear = table->
linear;
13875 for (i = 0; i < wordsPerRow; i++) {
13876 linear[xstart+i] ^= linear[ystart+i];
14036 unsigned int live = table->
keys - table->
dead;
14052 table->nodesDropped++;
14099 unsigned int live = table->
keys - table->
dead;
14115 table->nodesDropped++;
14166 table->nodesDropped++;
14172 stack[SP++] =
cuddE(N);
14231 double initialDead = table->
dead;
14302 stack[SP++] =
cuddE(N);
14330 #ifndef DD_NO_DEATH_ROW 14334 for (i = table->
deathRowDepth/4; i < table->deathRowDepth; i++) {
14335 if (table->
deathRow[i] == NULL)
break;
14368 #ifndef DD_NO_DEATH_ROW 14372 if (table->
deathRow[i] == NULL)
break;
14469 #define DD_MAX_SUBTABLE_SPARSITY 8 14491 int ddTotalNISwaps;
14565 unsigned int nextDyn;
14567 unsigned int initialSize;
14568 unsigned int finalSize;
14570 unsigned long localTime;
14573 if (table->
keys - table->
dead < (
unsigned) minsize)
14592 while (hook != NULL) {
14593 int res = (hook->
f)(table,
"BDD", (
void *)heuristic);
14594 if (res == 0)
return(0);
14606 ddTotalNISwaps = 0;
14608 switch(heuristic) {
14611 (void) fprintf(table->
out,
"#:I_RANDOM ");
14619 (void) fprintf(table->
out,
"#:I_SIFTING ");
14627 (void) fprintf(table->
out,
"#:I_WINDOW ");
14630 (void) fprintf(table->
out,
"#:I_ANNEAL ");
14633 (void) fprintf(table->
out,
"#:I_GENETIC ");
14637 (void) fprintf(table->
out,
"#:I_LINSIFT ");
14640 (void) fprintf(table->
out,
"#:I_EXACT ");
14645 (void) fprintf(table->
out,
"%8d: initial size",initialSize);
14659 (void) fprintf(table->
out,
"\n");
14661 (void) fprintf(table->
out,
"#:F_REORDER %8d: final size\n",finalSize);
14662 (void) fprintf(table->
out,
"#:T_REORDER %8g: total time (sec)\n",
14664 (void) fprintf(table->
out,
"#:N_REORDER %8d: total swaps\n",
14666 (void) fprintf(table->
out,
"#:M_REORDER %8d: NI swaps\n",ddTotalNISwaps);
14693 while (hook != NULL) {
14694 int res = (hook->
f)(table,
"BDD", (
void *)localTime);
14695 if (res == 0)
return(0);
14741 MMoutOfMemory = saveHandler;
14742 if (mem == NULL && table->
stash != NULL) {
14744 table->
stash = NULL;
14748 for (i = 0; i < table->
size; i++) {
14761 (void) fprintf(table->
err,
14762 "cuddDynamicAllocNode: out of memory");
14763 (void) fprintf(table->
err,
"Memory in use = %lu\n",
14768 unsigned long offset;
14777 offset = (
unsigned long) mem & (
sizeof(
DdNode) - 1);
14780 assert(((
unsigned long) mem & (
sizeof(
DdNode) - 1)) == 0);
14786 list[i - 1].
ref = 0;
14787 list[i - 1].
next = &list[i];
14838 size = table->
size;
14843 if (
entry == NULL) {
14845 goto cuddSiftingOutOfMem;
14847 var =
ALLOC(
int,size);
14850 goto cuddSiftingOutOfMem;
14853 for (i = 0; i < size; i++) {
14854 x = table->
perm[i];
14870 x = table->
perm[var[i]];
14878 if (!result)
goto cuddSiftingOutOfMem;
14880 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
14881 (void) fprintf(table->
out,
"-");
14882 }
else if (table->
keys > (
unsigned) previousSize + table->
isolated) {
14883 (void) fprintf(table->
out,
"+");
14884 (void) fprintf(table->
err,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keys - table->
isolated, var[i]);
14886 (void) fprintf(table->
out,
"=");
14888 fflush(table->
out);
14897 cuddSiftingOutOfMem:
14900 if (var != NULL)
FREE(var);
14938 Move *moves, *move;
14945 assert(lower >= 0 && upper < table->size && lower <= upper);
14948 nvars = upper - lower + 1;
14951 for (i = 0; i < iterate; i++) {
14956 for (j = lower; j <= upper; j++) {
14963 modulo = upper - pivot;
14970 modulo = pivot - lower - 1;
14986 if (moves == NULL)
goto cuddSwappingOutOfMem;
14988 if (!result)
goto cuddSwappingOutOfMem;
14989 while (moves != NULL) {
14990 move = moves->
next;
14995 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
14996 (void) fprintf(table->
out,
"-");
14997 }
else if (table->
keys > (
unsigned) previousSize + table->
isolated) {
14998 (void) fprintf(table->
out,
"+");
15000 (void) fprintf(table->
out,
"=");
15002 fflush(table->
out);
15005 (void) fprintf(table->
out,
"#:t_SWAPPING %8d: tmp size\n",
15012 cuddSwappingOutOfMem:
15013 while (moves != NULL) {
15014 move = moves->
next;
15088 int xindex, yindex;
15089 int xslots, yslots;
15090 int xshift, yshift;
15091 int oldxkeys, oldykeys;
15092 int newxkeys, newykeys;
15093 int comple, newcomplement;
15099 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
15140 newxkeys = oldxkeys;
15141 newykeys = oldykeys;
15144 newykeys = oldykeys;
15152 isolated = - ((table->
vars[xindex]->
ref == 1) +
15153 (table->
vars[yindex]->
ref == 1));
15160 if ((oldxkeys >= xslots || (
unsigned) xslots == table->
initSlots) &&
15162 for (i = 0; i < xslots; i++) {
15163 previousP = &(xlist[i]);
15165 while (f != sentinel) {
15173 previousP = &(f->
next);
15181 *previousP = sentinel;
15186 unsigned int newxslots;
15190 for (i = 0; i < xslots; i++) {
15192 while (f != sentinel) {
15210 newxshift = xshift;
15211 newxslots = xslots;
15216 while ((
unsigned) oldxkeys < newxslots &&
15225 MMoutOfMemory = saveHandler;
15226 if (newxlist == NULL) {
15227 (void) fprintf(table->
err,
"Unable to resize subtable %d for lack of memory\n", i);
15229 newxslots = xslots;
15230 newxshift = xshift;
15232 table->
slots += ((int) newxslots - xslots);
15239 ((
int) newxslots - xslots) *
sizeof(
DdNodePtr);
15241 xslots = newxslots;
15242 xshift = newxshift;
15246 for (i = 0; i < xslots; i++) {
15247 xlist[i] = sentinel;
15251 while (f != NULL) {
15256 posn =
ddHash(f1, f0, xshift);
15258 previousP = &(xlist[posn]);
15260 while (f1 <
cuddT(tmp)) {
15261 previousP = &(tmp->
next);
15264 while (f1 ==
cuddT(tmp) && f0 <
cuddE(tmp)) {
15265 previousP = &(tmp->
next);
15268 f->
next = *previousP;
15275 table->swapSteps += oldxkeys - newxkeys;
15282 while (f != NULL) {
15289 if ((
int) f1->
index == yindex) {
15300 if ((
int) f0->
index == yindex) {
15317 posn =
ddHash(f11, f01, xshift);
15319 previousP = &(xlist[posn]);
15320 newf1 = *previousP;
15321 while (f11 <
cuddT(newf1)) {
15322 previousP = &(newf1->
next);
15323 newf1 = *previousP;
15325 while (f11 ==
cuddT(newf1) && f01 <
cuddE(newf1)) {
15326 previousP = &(newf1->
next);
15327 newf1 = *previousP;
15329 if (
cuddT(newf1) == f11 &&
cuddE(newf1) == f01) {
15334 goto cuddSwapOutOfMem;
15335 newf1->
index = xindex; newf1->
ref = 1;
15336 cuddT(newf1) = f11;
15337 cuddE(newf1) = f01;
15342 newf1->
next = *previousP;
15343 *previousP = newf1;
15366 if (newcomplement) {
15371 posn =
ddHash(f10, f00, xshift);
15373 previousP = &(xlist[posn]);
15374 newf0 = *previousP;
15375 while (f10 <
cuddT(newf0)) {
15376 previousP = &(newf0->
next);
15377 newf0 = *previousP;
15379 while (f10 ==
cuddT(newf0) && f00 <
cuddE(newf0)) {
15380 previousP = &(newf0->
next);
15381 newf0 = *previousP;
15383 if (
cuddT(newf0) == f10 &&
cuddE(newf0) == f00) {
15388 goto cuddSwapOutOfMem;
15389 newf0->
index = xindex; newf0->
ref = 1;
15390 cuddT(newf0) = f10;
15391 cuddE(newf0) = f00;
15396 newf0->
next = *previousP;
15397 *previousP = newf0;
15402 if (newcomplement) {
15412 posn =
ddHash(newf1, newf0, yshift);
15414 previousP = &(ylist[posn]);
15416 while (newf1 <
cuddT(tmp)) {
15417 previousP = &(tmp->
next);
15420 while (newf1 ==
cuddT(tmp) && newf0 <
cuddE(tmp)) {
15421 previousP = &(tmp->
next);
15424 f->
next = *previousP;
15432 for (i = 0; i < yslots; i++) {
15433 previousP = &(ylist[i]);
15435 while (f != sentinel) {
15446 previousP = &(f->
next);
15450 *previousP = sentinel;
15455 (void) fprintf(table->
out,
"Swapping %d and %d\n",x,y);
15459 for (i = 0; i < yslots; i++) {
15461 while (f != sentinel) {
15468 if (count != newykeys) {
15469 (void) fprintf(table->
out,
15470 "Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",
15471 oldykeys,newykeys,count);
15474 (void) fprintf(table->
out,
15475 "Error in id's of ylist\twrong id's = %d\n",
15479 for (i = 0; i < xslots; i++) {
15481 while (f != sentinel) {
15488 if (count != newxkeys) {
15489 (void) fprintf(table->
out,
15490 "Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",
15491 oldxkeys,newxkeys,count);
15494 (void) fprintf(table->
out,
15495 "Error in id's of xlist\twrong id's = %d\n",
15499 isolated += (table->
vars[xindex]->
ref == 1) +
15500 (table->
vars[yindex]->
ref == 1);
15533 table->
perm[xindex] = y; table->
perm[yindex] = x;
15536 table->
keys += newxkeys + newykeys - oldxkeys - oldykeys;
15541 (void) fprintf(table->
err,
"Error: cuddSwapInPlace out of memory\n");
15581 if (table->
size == 0)
15592 if (invperm == NULL) {
15596 for (i = 0; i < table->
sizeZ; i += M) {
15598 int index = indexZ / M;
15599 invperm[i / M] = index;
15608 for (i = 0; i < table->
size; i++) {
15614 if (result == 0)
return(0);
15650 return((*ptrX) - (*ptrY));
15673 Move *move, *moves;
15681 tmp = x; x = y; y = tmp;
15684 xRef = x; yRef = y;
15692 if ( xNext == yNext) {
15694 if (size == 0)
goto ddSwapAnyOutOfMem;
15696 if (move == NULL)
goto ddSwapAnyOutOfMem;
15700 move->
next = moves;
15704 if (size == 0)
goto ddSwapAnyOutOfMem;
15706 if (move == NULL)
goto ddSwapAnyOutOfMem;
15710 move->
next = moves;
15714 if (size == 0)
goto ddSwapAnyOutOfMem;
15716 if (move == NULL)
goto ddSwapAnyOutOfMem;
15720 move->
next = moves;
15723 tmp = x; x = y; y = tmp;
15725 }
else if (x == yNext) {
15728 if (size == 0)
goto ddSwapAnyOutOfMem;
15730 if (move == NULL)
goto ddSwapAnyOutOfMem;
15734 move->
next = moves;
15737 tmp = x; x = y; y = tmp;
15741 if (size == 0)
goto ddSwapAnyOutOfMem;
15743 if (move == NULL)
goto ddSwapAnyOutOfMem;
15747 move->
next = moves;
15751 if (size == 0)
goto ddSwapAnyOutOfMem;
15753 if (move == NULL)
goto ddSwapAnyOutOfMem;
15757 move->
next = moves;
15766 if (xNext > yRef)
break;
15768 if ((
double) size > table->
maxGrowth * (
double) limitSize)
break;
15769 if (size < limitSize) limitSize = size;
15773 if (size == 0)
goto ddSwapAnyOutOfMem;
15775 if (move == NULL)
goto ddSwapAnyOutOfMem;
15779 move->
next = moves;
15786 while (moves != NULL) {
15787 move = moves->
next;
15833 if (!result)
goto ddSiftingAuxOutOfMem;
15835 }
else if (x == xHigh) {
15841 if (!result)
goto ddSiftingAuxOutOfMem;
15843 }
else if ((x - xLow) > (xHigh - x)) {
15847 if (moveDown != NULL) {
15851 if (moveUp == (
Move *) CUDD_OUT_OF_MEM)
goto ddSiftingAuxOutOfMem;
15854 if (!result)
goto ddSiftingAuxOutOfMem;
15860 if (moveUp != NULL) {
15864 if (moveDown == (
Move *) CUDD_OUT_OF_MEM)
goto ddSiftingAuxOutOfMem;
15867 if (!result)
goto ddSiftingAuxOutOfMem;
15870 while (moveDown != NULL) {
15871 move = moveDown->
next;
15875 while (moveUp != NULL) {
15876 move = moveUp->
next;
15883 ddSiftingAuxOutOfMem:
15885 while (moveDown != NULL) {
15886 move = moveDown->
next;
15891 if (moveUp != (
Move *) CUDD_OUT_OF_MEM) {
15892 while (moveUp != NULL) {
15893 move = moveUp->
next;
15926 int xindex, yindex;
15945 for (x = xLow + 1; x < y; x++) {
15948 isolated = table->
vars[xindex]->
ref == 1;
15952 isolated = table->
vars[yindex]->
ref == 1;
15956 while (x >= xLow && L <= limitSize) {
15960 for (z = xLow + 1; z < y; z++) {
15963 isolated = table->
vars[zindex]->
ref == 1;
15967 isolated = table->
vars[yindex]->
ref == 1;
15972 if (size == 0)
goto ddSiftingUpOutOfMem;
15975 isolated = table->
vars[xindex]->
ref == 1;
15979 if (move == NULL)
goto ddSiftingUpOutOfMem;
15983 move->
next = moves;
15985 if ((
double) size > (double) limitSize * table->
maxGrowth)
break;
15986 if (size < limitSize) limitSize = size;
15992 ddSiftingUpOutOfMem:
15993 while (moves != NULL) {
15994 move = moves->
next;
16027 int xindex, yindex;
16040 for (y = xHigh; y > x; y--) {
16043 isolated = table->
vars[yindex]->
ref == 1;
16049 while (y <= xHigh && size - R < limitSize) {
16052 for (z = xHigh; z > x; z--) {
16055 isolated = table->
vars[zindex]->
ref == 1;
16064 isolated = table->
vars[yindex]->
ref == 1;
16068 if (size == 0)
goto ddSiftingDownOutOfMem;
16070 if (move == NULL)
goto ddSiftingDownOutOfMem;
16074 move->
next = moves;
16076 if ((
double) size > (double) limitSize * table->
maxGrowth)
break;
16077 if (size < limitSize) limitSize = size;
16083 ddSiftingDownOutOfMem:
16084 while (moves != NULL) {
16085 move = moves->
next;
16116 for (move = moves; move != NULL; move = move->
next) {
16117 if (move->
size < size) {
16122 for (move = moves; move != NULL; move = move->
next) {
16123 if (move->
size == size)
return(1);
16125 if (!res)
return(0);
16162 for (i = 0; i < table->
size; i++) {
16168 if (res == 0)
return(0);
16190 (void) fflush(table->
out);
16228 unsigned long localTime;
16238 (void) fprintf(table->
out,
"#:I_SHUFFLE %8d: initial size\n",
16240 ddTotalNISwaps = 0;
16243 numvars = table->
size;
16245 for (level = 0; level <
numvars; level++) {
16246 index = permutation[level];
16247 position = table->
perm[index];
16251 result =
ddSiftUp2(table,position,level);
16252 if (!result)
return(0);
16254 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
16255 (void) fprintf(table->
out,
"-");
16256 }
else if (table->
keys > (
unsigned) previousSize + table->
isolated) {
16257 (void) fprintf(table->
out,
"+");
16259 (void) fprintf(table->
out,
"=");
16261 fflush(table->
out);
16266 (void) fprintf(table->
out,
"\n");
16268 (void) fprintf(table->
out,
"#:F_SHUFFLE %8d: final size\n",finalSize);
16269 (void) fprintf(table->
out,
"#:T_SHUFFLE %8g: total time (sec)\n",
16271 (void) fprintf(table->
out,
"#:N_SHUFFLE %8d: total swaps\n",
16273 (void) fprintf(table->
out,
"#:M_SHUFFLE %8d: NI swaps\n",ddTotalNISwaps);
16304 while (y >= xLow) {
16335 if (treenode == NULL)
return;
16336 treenode->
low = ((int) treenode->
index < table->
size) ?
16338 if (treenode->
child != NULL) {
16341 if (treenode->
younger != NULL)
16371 unsigned int i, size;
16372 int index, level, minLevel, maxLevel, minIndex;
16374 if (treenode == NULL)
return(1);
16380 for (i = treenode->
low; i < treenode->low + treenode->
size; i++) {
16382 level = perm[index];
16383 if (level < minLevel) {
16387 if (level > maxLevel)
16390 size = maxLevel - minLevel + 1;
16391 if (minIndex == -1)
return(0);
16392 if (size == treenode->
size) {
16393 treenode->
low = minLevel;
16394 treenode->
index = minIndex;
16399 if (treenode->
child != NULL) {
16403 if (treenode->
younger != NULL) {
16430 unsigned int i, size;
16431 int index, level, minLevel, maxLevel;
16433 if (treenode == NULL)
return(1);
16435 minLevel = table->
size;
16438 for (i = treenode->
low; i < treenode->low + treenode->
size; i++) {
16440 level = perm[index];
16441 if (level < minLevel)
16443 if (level > maxLevel)
16446 size = maxLevel - minLevel + 1;
16447 if (size != treenode->
size)
16450 if (treenode->
child != NULL) {
16454 if (treenode->
younger != NULL) {
16539 #define DD_BIGGY 100000000 16568 #define WEIGHT(weight, col) ((weight) == NULL ? 1 : weight[col]) 16625 int complement, cost;
16630 if (f ==
Cudd_Not(one) || f == zero) {
16631 if (length != NULL) {
16651 if (!
st_lookup(visited, F, &rootPair))
return(NULL);
16654 cost = rootPair->
neg;
16656 cost = rootPair->
pos;
16660 sol =
getCube(manager,visited,f,cost);
16667 if (length != NULL) {
16696 unsigned int topf, level;
16697 DdNode *F, *fv, *fvn, *res;
16702 assert(0 <= i && i < dd->size);
16711 level = (unsigned) dd->
perm[i];
16712 if (topf > level) {
16732 if (topf == (
unsigned) level) {
16744 if (res ==
DD_ONE(dd)) {
16776 DdNode *tmp, *One, *Gr, *Dr;
16777 DdNode *Fv, *Fvn, *Gv, *Gvn, *Dv, *Dvn;
16779 unsigned int flevel, glevel, dlevel, top;
16785 if (D == One || F == G)
return(1);
16805 if (tmp != NULL)
return(tmp == One);
16811 top =
ddMin(flevel,glevel);
16814 top =
ddMin(top,dlevel);
16817 if (top == flevel) {
16823 if (top == glevel) {
16833 if (top == dlevel) {
16876 DdNode *tmp, *One, *F, *G;
16877 DdNode *Ft, *Fe, *Gt, *Ge, *Dt, *De;
16879 unsigned int flevel, glevel, dlevel, top;
16886 if (f == g || g == One || f ==
Cudd_Not(One) || D == One ||
16887 D == f || D ==
Cudd_Not(g))
return(1);
16976 if (tmp != NULL)
return(tmp == One);
16983 top =
ddMin(flevel,glevel);
16985 top =
ddMin(top,dlevel);
16988 if (top == flevel) {
16998 if (top == glevel) {
17008 if (top == dlevel) {
17051 DdNode *fv, *fvn, *gv, *gvn, *r;
17052 unsigned int topf, topg;
17056 if (f == g)
return(1);
17062 (void) fprintf(dd->
out,
"Offending nodes:\n");
17063 (void) fprintf(dd->
out,
17064 "f: address = %p\t value = %40.30f\n",
17065 (
void *) f,
cuddV(f));
17066 (void) fprintf(dd->
out,
17067 "g: address = %p\t value = %40.30f\n",
17068 (
void *) g,
cuddV(g));
17085 if (topf <= topg) {fv =
cuddT(f); fvn =
cuddE(f);}
else {fv = fvn = f;}
17086 if (topg <= topf) {gv =
cuddT(g); gvn =
cuddE(g);}
else {gv = gvn = g;}
17164 if (expanded == NULL) {
17178 }
else if (e == zero) {
17186 if (scan ==
DD_ONE(dd)) {
17253 DdNode *my_root, *T, *E;
17258 if (
st_lookup(visited, my_root, &my_pair)) {
17260 res_pair.
pos = my_pair->
neg;
17261 res_pair.
neg = my_pair->
pos;
17263 res_pair.
pos = my_pair->
pos;
17264 res_pair.
neg = my_pair->
neg;
17275 if (my_root != zero) {
17283 T =
cuddT(my_root);
17284 E =
cuddE(my_root);
17293 if (support != NULL) {
17294 support[my_root->
index] = 1;
17299 if (my_pair == NULL) {
17301 int tmp = res_pair.
pos;
17302 res_pair.
pos = res_pair.
neg;
17303 res_pair.
neg = tmp;
17307 my_pair->
pos = res_pair.
pos;
17308 my_pair->
neg = res_pair.
neg;
17310 st_insert(visited, (
char *)my_root, (
char *)my_pair);
17312 res_pair.
pos = my_pair->neg;
17313 res_pair.
neg = my_pair->pos;
17315 res_pair.
pos = my_pair->pos;
17316 res_pair.
neg = my_pair->neg;
17352 DdNode *my_root, *T, *E;
17356 if (
st_lookup(visited, my_root, &my_pair)) {
17358 res_pair.
pos = my_pair->
neg;
17359 res_pair.
neg = my_pair->
pos;
17361 res_pair.
pos = my_pair->
pos;
17362 res_pair.
neg = my_pair->
neg;
17373 if (my_root != zero) {
17381 T =
cuddT(my_root);
17382 E =
cuddE(my_root);
17391 if (my_pair == NULL) {
17393 int tmp = res_pair.
pos;
17394 res_pair.
pos = res_pair.
neg;
17395 res_pair.
neg = tmp;
17399 my_pair->
pos = res_pair.
pos;
17400 my_pair->
neg = res_pair.
neg;
17403 st_insert(visited, (
char *)my_root, (
char *)my_pair);
17405 res_pair.
pos = my_pair->neg;
17406 res_pair.
neg = my_pair->pos;
17408 res_pair.
pos = my_pair->pos;
17409 res_pair.
neg = my_pair->neg;
17495 (void) fprintf(manager->
err,
"We shouldn't be here!\n");
17527 DdNode *
one, *
zero, *lbv, *lbvn, *lbnx, *ubv, *ubvn, *fv, *fvn, *res;
17528 DdNode *F, *UB, *LB, *t, *e;
17529 unsigned int top, toplb, topub, topf, index;
17535 assert(ub != zero && lb != zero);
17543 if (ub == f || f == one)
return(ub);
17544 if (lb == f)
return(lb);
17571 top =
ddMin(topf,toplb);
17572 if (toplb == top) {
17587 lbnx = lbv = lbvn = lb;
17589 if (topub == top) {
17613 if (t == NULL)
return(NULL);
17615 assert(topub == toplb && topub == top && lbv == zero);
17625 if (ubv == ubvn && fv == fvn) {
17628 if (ubvn != zero) {
17635 assert(topub == toplb && topub == top && lbvn == zero);
17644 if (toplb == top) {
17651 if (newT == NULL) {
17659 if (newT == NULL) {
17669 }
else if (lbvn == zero) {
17674 if (newE == NULL) {
17736 int positive, l, lT, lE;
17746 }
else if (f == zero) {
17758 positive = phases[F->
index];
17759 l = positive ?
ddMin(lT+1, lE) :
ddMin(lT, lE+1);
17842 #define MV_OOM (Move *)1 17864 extern int ddTotalNISwaps;
17917 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
17943 if (table->
vars[yindex]->
ref == 1)
17947 xsymmy = xsymmyp = 1;
17951 for (i = 0; i < slots; i++) {
17953 while (f != sentinel) {
17958 if ((
int) f1->
index == yindex) {
17962 if ((
int) f0->
index != yindex) {
17971 if ((
int) f0->
index == yindex) {
17983 xsymmy &= f01 == f10;
17984 xsymmyp &= f11 == f00;
17985 if ((xsymmy == 0) && (xsymmyp == 0))
17994 TotalRefCount = -1;
17997 for (i = 0; i < slots; i++) {
17999 while (f != sentinel) {
18000 TotalRefCount += f->
ref;
18005 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 18006 if (arccount == TotalRefCount) {
18008 (void) fprintf(table->
out,
18009 "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
18010 xindex,yindex,x,y);
18014 return(arccount == TotalRefCount);
18058 size = table->
size;
18063 if (
entry == NULL) {
18065 goto ddSymmSiftingOutOfMem;
18067 var =
ALLOC(
int,size);
18070 goto ddSymmSiftingOutOfMem;
18073 for (i = 0; i < size; i++) {
18074 x = table->
perm[i];
18082 for (i = lower; i <= upper; i++) {
18093 x = table->
perm[var[i]];
18097 if (x < lower || x > upper)
continue;
18100 if (!result)
goto ddSymmSiftingOutOfMem;
18102 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
18103 (void) fprintf(table->
out,
"-");
18104 }
else if (table->
keys > (
unsigned) previousSize +
18106 (void) fprintf(table->
out,
"+");
18108 (void) fprintf(table->
out,
"=");
18110 fflush(table->
out);
18121 (void) fprintf(table->
out,
"\n#:S_SIFTING %8d: symmetric variables\n",
18123 (void) fprintf(table->
out,
"#:G_SIFTING %8d: symmetric groups",
18129 ddSymmSiftingOutOfMem:
18132 if (var != NULL)
FREE(var);
18183 size = table->
size;
18188 if (
entry == NULL) {
18190 goto ddSymmSiftingConvOutOfMem;
18192 var =
ALLOC(
int,size);
18195 goto ddSymmSiftingConvOutOfMem;
18198 for (i = 0; i < size; i++) {
18199 x = table->
perm[i];
18209 for (i = lower; i <= upper; i++) {
18220 x = table->
perm[var[i]];
18221 if (x < lower || x > upper)
continue;
18228 if (!result)
goto ddSymmSiftingConvOutOfMem;
18230 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
18231 (void) fprintf(table->
out,
"-");
18232 }
else if (table->
keys > (
unsigned) previousSize +
18234 (void) fprintf(table->
out,
"+");
18236 (void) fprintf(table->
out,
"=");
18238 fflush(table->
out);
18244 while ((
unsigned) initialSize > table->
keys - table->
isolated) {
18247 (void) fprintf(table->
out,
"\n");
18250 for (x = lower, classes = 0; x <= upper; x++, classes++) {
18263 qsort((
void *)var,classes,
sizeof(
int),(
DD_QSFP)ddSymmUniqueCompare);
18273 x = table->
perm[var[i]];
18279 if (!result )
goto ddSymmSiftingConvOutOfMem;
18281 if (table->
keys < (
unsigned) previousSize + table->
isolated) {
18282 (void) fprintf(table->
out,
"-");
18283 }
else if (table->
keys > (
unsigned) previousSize +
18285 (void) fprintf(table->
out,
"+");
18287 (void) fprintf(table->
out,
"=");
18289 fflush(table->
out);
18298 (void) fprintf(table->
out,
"\n#:S_SIFTING %8d: symmetric variables\n",
18300 (void) fprintf(table->
out,
"#:G_SIFTING %8d: symmetric groups",
18309 ddSymmSiftingConvOutOfMem:
18312 if (var != NULL)
FREE(var);
18343 return((*ptrX) - (*ptrY));
18378 int initGroupSize, finalGroupSize;
18391 if ((x - xLow) > (xHigh - x)) {
18395 for (i = x; i > xLow; i--) {
18408 for (i = x; i < xHigh; i++) {
18413 while ((
unsigned) topbot < table->subtables[topbot].next) {
18425 while ((
unsigned) x < table->subtables[x].next)
18434 if (x == xHigh)
return(1);
18440 if (moveDown ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18441 if (moveDown == NULL)
return(1);
18446 while ((
unsigned) i < table->subtables[i].next) {
18454 finalGroupSize = i - x + 1;
18456 if (initGroupSize == finalGroupSize) {
18464 if (!result)
goto ddSymmSiftingAuxOutOfMem;
18471 if (x == xLow)
return(1);
18473 initGroupSize = i - x + 1;
18477 if (moveUp ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18478 if (moveUp == NULL)
return(1);
18488 finalGroupSize = x - i + 1;
18490 if (initGroupSize == finalGroupSize) {
18498 if (!result)
goto ddSymmSiftingAuxOutOfMem;
18500 }
else if ((x - xLow) > (xHigh - x)) {
18504 if (moveDown ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18506 if (moveDown != NULL) {
18509 while ((
unsigned) i < table->subtables[i].next) {
18514 while ((
unsigned) i < table->subtables[i].next) {
18524 initGroupSize = i - x + 1;
18527 if (moveUp ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18529 if (moveUp != NULL) {
18534 while ((
unsigned) x < table->subtables[x].next)
18542 finalGroupSize = x - i + 1;
18544 if (initGroupSize == finalGroupSize) {
18548 while (moveDown != NULL) {
18549 move = moveDown->
next;
18557 if (!result)
goto ddSymmSiftingAuxOutOfMem;
18565 if (moveUp ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18567 if (moveUp != NULL) {
18571 while ((
unsigned) x < table->subtables[x].next)
18580 initGroupSize = x - i + 1;
18583 if (moveDown ==
MV_OOM)
goto ddSymmSiftingAuxOutOfMem;
18585 if (moveDown != NULL) {
18588 while ((
unsigned) i < table->subtables[i].next) {
18600 finalGroupSize = i - x + 1;
18602 if (initGroupSize == finalGroupSize) {
18606 while (moveUp != NULL) {
18607 move = moveUp->
next;
18615 if (!result)
goto ddSymmSiftingAuxOutOfMem;
18618 while (moveDown != NULL) {
18619 move = moveDown->
next;
18623 while (moveUp != NULL) {
18624 move = moveUp->
next;
18631 ddSymmSiftingAuxOutOfMem:
18632 if (moveDown !=
MV_OOM) {
18633 while (moveDown != NULL) {
18634 move = moveDown->
next;
18640 while (moveUp != NULL) {
18641 move = moveUp->
next;
18679 int initGroupSize, finalGroupSize;
18693 initGroupSize = x - i + 1;
18697 if (moveDown ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18698 if (moveDown == NULL)
return(1);
18702 while ((
unsigned) i < table->subtables[i].next) {
18710 finalGroupSize = i - x + 1;
18712 if (initGroupSize == finalGroupSize) {
18720 if (!result)
goto ddSymmSiftingConvAuxOutOfMem;
18724 while ((
unsigned) x < table->subtables[x].next)
18729 if (x == xLow)
return(1);
18731 initGroupSize = i - x + 1;
18735 if (moveUp ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18736 if (moveUp == NULL)
return(1);
18745 finalGroupSize = x - i + 1;
18747 if (initGroupSize == finalGroupSize) {
18756 goto ddSymmSiftingConvAuxOutOfMem;
18758 }
else if ((x - xLow) > (xHigh - x)) {
18761 if (moveDown ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18763 if (moveDown != NULL) {
18766 while ((
unsigned) i < table->subtables[i].next) {
18770 while ((
unsigned) x < table->subtables[x].next)
18780 initGroupSize = i - x + 1;
18783 if (moveUp ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18785 if (moveUp != NULL) {
18790 while ((
unsigned) x < table->subtables[x].next)
18798 finalGroupSize = x - i + 1;
18800 if (initGroupSize == finalGroupSize) {
18804 while (moveDown != NULL) {
18805 move = moveDown->
next;
18813 if (!result)
goto ddSymmSiftingConvAuxOutOfMem;
18821 if (moveUp ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18823 if (moveUp != NULL) {
18828 while ((
unsigned) x < table->subtables[x].next)
18836 initGroupSize = x - i + 1;
18839 if (moveDown ==
MV_OOM)
goto ddSymmSiftingConvAuxOutOfMem;
18841 if (moveDown != NULL) {
18844 while ((
unsigned) i < table->subtables[i].next) {
18856 finalGroupSize = i - x + 1;
18858 if (initGroupSize == finalGroupSize) {
18862 while (moveUp != NULL) {
18863 move = moveUp->
next;
18871 if (!result)
goto ddSymmSiftingConvAuxOutOfMem;
18874 while (moveDown != NULL) {
18875 move = moveDown->
next;
18879 while (moveUp != NULL) {
18880 move = moveUp->
next;
18887 ddSymmSiftingConvAuxOutOfMem:
18888 if (moveDown !=
MV_OOM) {
18889 while (moveDown != NULL) {
18890 move = moveDown->
next;
18896 while (moveUp != NULL) {
18897 move = moveUp->
next;
18936 int xindex, yindex;
18957 while ((
unsigned) gybot < table->subtables[gybot].next)
18959 for (z = xLow + 1; z <= gybot; z++) {
18962 isolated = table->
vars[zindex]->
ref == 1;
18968 while (x >= xLow && L <= limitSize) {
18971 while ((
unsigned) gybot < table->subtables[gybot].next)
18974 for (z = xLow + 1; z <= gybot; z++) {
18977 isolated = table->
vars[zindex]->
ref == 1;
19000 if (size == 0)
goto ddSymmSiftingUpOutOfMem;
19003 isolated = table->
vars[xindex]->
ref == 1;
19007 if (move == NULL)
goto ddSymmSiftingUpOutOfMem;
19011 move->
next = moves;
19013 if ((
double) size > (double) limitSize * table->
maxGrowth)
19015 if (size < limitSize) limitSize = size;
19018 if (size == 0)
goto ddSymmSiftingUpOutOfMem;
19024 isolated = table->
vars[zindex]->
ref == 1;
19028 }
while (z != (
int) moves->
y);
19029 if ((
double) size > (
double) limitSize * table->
maxGrowth)
19031 if (size < limitSize) limitSize = size;
19039 ddSymmSiftingUpOutOfMem:
19040 while (moves != NULL) {
19041 move = moves->
next;
19078 int xindex, yindex;
19092 for (z = xHigh; z > gxtop; z--) {
19095 isolated = table->
vars[zindex]->
ref == 1;
19101 while (y <= xHigh && size - R < limitSize) {
19105 for (z = xHigh; z > gxtop; z--) {
19108 isolated = table->
vars[zindex]->
ref == 1;
19128 isolated = table->
vars[yindex]->
ref == 1;
19136 if (size == 0)
goto ddSymmSiftingDownOutOfMem;
19138 if (move == NULL)
goto ddSymmSiftingDownOutOfMem;
19142 move->
next = moves;
19144 if ((
double) size > (double) limitSize * table->
maxGrowth)
19146 if (size < limitSize) limitSize = size;
19154 isolated = table->
vars[zindex]->
ref == 1;
19158 }
while (z <= gybot);
19160 if (size == 0)
goto ddSymmSiftingDownOutOfMem;
19161 if ((
double) size > (
double) limitSize * table->
maxGrowth)
19163 if (size < limitSize) limitSize = size;
19166 for (z = gxtop + 1; z <= gybot; z++) {
19169 isolated = table->
vars[zindex]->
ref == 1;
19180 ddSymmSiftingDownOutOfMem:
19181 while (moves != NULL) {
19182 move = moves->
next;
19213 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
19222 xsize = xbot - xtop + 1;
19224 while ((
unsigned) ybot < table->subtables[ybot].next)
19227 ysize = ybot - ytop + 1;
19230 for (i = 1; i <= ysize; i++) {
19231 for (j = 1; j <= xsize; j++) {
19233 if (size == 0)
return(0);
19234 swapx = x; swapy = y;
19244 for (i = 0; i < ysize-1 ; i++) {
19252 for (i = 0; i < xsize - 1 ; i++) {
19260 if (move == NULL)
return(0);
19264 move->
next = *moves;
19292 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
19301 xsize = xbot - xtop + 1;
19303 while ((
unsigned) ybot < table->subtables[ybot].next)
19306 ysize = ybot - ytop + 1;
19309 for (i = 1; i <= ysize; i++) {
19310 for (j = 1; j <= xsize; j++) {
19312 if (size == 0)
return(0);
19322 for (i = 0; i < ysize-1 ; i++) {
19330 for (i = 0; i < xsize-1 ; i++) {
19364 for (move = moves; move != NULL; move = move->
next) {
19365 if (move->
size < size) {
19370 for (move = moves; move != NULL; move = move->
next) {
19371 if (move->
size == size)
return(1);
19381 if (!res)
return(0);
19409 int TotalSymmGroups = 0;
19411 for (i = lower; i <= upper; i++) {
19426 *symvars = TotalSymm;
19427 *symgroups = TotalSymmGroups;
19521 #ifndef DD_UNSORTED_FREE_LIST 19522 #ifdef DD_RED_BLACK_FREE_LIST 19524 #define DD_STACK_SIZE 128 19527 #define DD_PAGE_SIZE 8192 19528 #define DD_PAGE_MASK ~(DD_PAGE_SIZE - 1) 19539 unsigned int bits[2];
19559 #ifndef DD_UNSORTED_FREE_LIST 19560 #ifdef DD_RED_BLACK_FREE_LIST 19562 #define DD_INSERT_COMPARE(x,y) \ 19563 (((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK)) 19564 #define DD_COLOR(p) ((p)->index) 19565 #define DD_IS_BLACK(p) ((p)->index == DD_BLACK) 19566 #define DD_IS_RED(p) ((p)->index == DD_RED) 19567 #define DD_LEFT(p) cuddT(p) 19568 #define DD_RIGHT(p) cuddE(p) 19569 #define DD_NEXT(p) ((p)->next) 19584 #ifdef DD_RED_BLACK_FREE_LIST 19587 static void cuddRotateLeft (
DdNodePtr *nodeP);
19588 static void cuddRotateRight (
DdNodePtr *nodeP);
19589 static void cuddDoRebalance (
DdNodePtr **stack,
int stackN);
19593 static int cuddCheckCollisionOrdering (
DdManager *unique,
int i,
int j);
19657 MMoutOfMemory = saveHandler;
19666 if (unique->
stash != NULL) {
19668 unique->
stash = NULL;
19682 (void) fprintf(unique->
err,
19683 "cuddAllocNode: out of memory");
19684 (void) fprintf(unique->
err,
"Memory in use = %lu\n",
19706 list[i - 1].
ref = 0;
19707 list[i - 1].
next = &list[i];
19739 unsigned int numVars ,
19740 unsigned int numVarsZ ,
19741 unsigned int numSlots ,
19742 unsigned int looseUpTo )
19748 unsigned int slots;
19751 if (unique == NULL) {
19756 sentinel->
index = 0;
19757 cuddT(sentinel) = NULL;
19758 cuddE(sentinel) = NULL;
19759 sentinel->
next = NULL;
19761 unique->
size = numVars;
19762 unique->
sizeZ = numVarsZ;
19768 while (slots < numSlots) {
19774 unique->
slots = (numVars + numVarsZ + 1) * slots;
19798 if (unique->
perm == NULL) {
19805 if (unique->
invperm == NULL) {
19813 if (unique->
permZ == NULL) {
19831 unique->
map = NULL;
19833 if (unique->
stack == NULL) {
19843 unique->
stack[0] = NULL;
19845 #ifndef DD_NO_DEATH_ROW 19866 for (i = 0; (unsigned) i < numVars; i++) {
19879 if (nodelist == NULL) {
19880 for (j = 0; j < i; j++) {
19893 for (j = 0; (unsigned) j < slots; j++) {
19894 nodelist[j] = sentinel;
19896 unique->
perm[i] = i;
19899 for (i = 0; (unsigned) i < numVarsZ; i++) {
19906 if (nodelist == NULL) {
19907 for (j = 0; (unsigned) j < numVars; j++) {
19911 for (j = 0; j < i; j++) {
19923 for (j = 0; (unsigned) j < slots; j++) {
19924 nodelist[j] = NULL;
19926 unique->
permZ[i] = i;
19935 if (nodelist == NULL) {
19936 for (j = 0; (unsigned) j < numVars; j++) {
19940 for (j = 0; (unsigned) j < numVarsZ; j++) {
19952 for (j = 0; (unsigned) j < slots; j++) {
19953 nodelist[j] = NULL;
19960 * (
sizeof(
DdSubtable) + 2 *
sizeof(
int)) + (numVars + 1) *
19963 #ifndef DD_NO_DEATH_ROW 19984 unique->
tree = NULL;
19985 unique->
treeZ = NULL;
20005 unique->
out = stdout;
20006 unique->
err = stderr;
20017 unique->nodesDropped = 0;
20018 unique->nodesFreed = 0;
20021 #ifdef DD_UNIQUE_PROFILE 20022 unique->uniqueLookUps = 0;
20023 unique->uniqueLinks = 0;
20026 unique->recursiveCalls = 0;
20027 unique->swapSteps = 0;
20029 unique->nextSample = 250000;
20058 while (memlist != NULL) {
20066 for (i = 0; i < unique->
size; i++) {
20069 for (i = 0; i < unique->
sizeZ; i++) {
20083 #ifndef DD_NO_DEATH_ROW 20128 int i, j, deleted, totalDeleted, totalDeletedZ;
20133 unsigned long localTime;
20134 #ifndef DD_UNSORTED_FREE_LIST 20135 #ifdef DD_RED_BLACK_FREE_LIST 20139 DdNode *downTrav, *sentry;
20144 #ifndef DD_NO_DEATH_ROW 20149 while (hook != NULL) {
20150 int res = (hook->
f)(unique,
"DD",NULL);
20151 if (res == 0)
return(0);
20155 if (unique->
dead + unique->
deadZ == 0) {
20157 while (hook != NULL) {
20158 int res = (hook->
f)(unique,
"DD",NULL);
20159 if (res == 0)
return(0);
20173 (void) fprintf(unique->
err,
"minDead = %d\n", unique->
minDead);
20183 (void) fprintf(unique->
err,
20184 "garbage collecting (%d dead BDD nodes out of %d, min %d)...",
20186 (void) fprintf(unique->
err,
20187 " (%d dead ZDD nodes out of %d)...",
20194 for (i = 0; i < slots; i++) {
20196 if (c->
data != NULL) {
20212 #ifndef DD_UNSORTED_FREE_LIST 20213 #ifdef DD_RED_BLACK_FREE_LIST 20218 for (i = 0; i < unique->
size; i++) {
20224 for (j = 0; j < slots; j++) {
20225 lastP = &(nodelist[j]);
20227 while (node != sentinel) {
20229 if (node->
ref == 0) {
20231 #ifndef DD_UNSORTED_FREE_LIST 20232 #ifdef DD_RED_BLACK_FREE_LIST 20233 cuddOrderedInsert(&tree,node);
20240 lastP = &(node->
next);
20249 totalDeleted += deleted;
20257 for (j = 0; j < slots; j++) {
20258 lastP = &(nodelist[j]);
20260 while (node != NULL) {
20262 if (node->
ref == 0) {
20264 #ifndef DD_UNSORTED_FREE_LIST 20265 #ifdef DD_RED_BLACK_FREE_LIST 20266 cuddOrderedInsert(&tree,node);
20273 lastP = &(node->
next);
20282 totalDeleted += deleted;
20286 if ((
unsigned) totalDeleted != unique->
dead) {
20289 unique->
keys -= totalDeleted;
20292 unique->nodesFreed += (double) totalDeleted;
20297 for (i = 0; i < unique->
sizeZ; i++) {
20303 for (j = 0; j < slots; j++) {
20304 lastP = &(nodelist[j]);
20306 while (node != NULL) {
20308 if (node->
ref == 0) {
20310 #ifndef DD_UNSORTED_FREE_LIST 20311 #ifdef DD_RED_BLACK_FREE_LIST 20312 cuddOrderedInsert(&tree,node);
20319 lastP = &(node->
next);
20328 totalDeletedZ += deleted;
20336 if ((
unsigned) totalDeletedZ != unique->
deadZ) {
20339 unique->
keysZ -= totalDeletedZ;
20342 unique->nodesFreed += (double) totalDeletedZ;
20346 #ifndef DD_UNSORTED_FREE_LIST 20347 #ifdef DD_RED_BLACK_FREE_LIST 20352 while (memListTrav != NULL) {
20357 downTrav = (
DdNode *)memListTrav;
20360 if (downTrav[k].ref == 0) {
20361 if (sentry == NULL) {
20362 unique->
nextFree = sentry = &downTrav[k];
20366 sentry = (sentry->
next = &downTrav[k]);
20370 memListTrav = nxtNode;
20372 sentry->
next = NULL;
20379 while (hook != NULL) {
20380 int res = (hook->
f)(unique,
"DD",NULL);
20381 if (res == 0)
return(0);
20386 (void) fprintf(unique->
err,
" done\n");
20389 return(totalDeleted+totalDeletedZ);
20502 unsigned int level;
20510 #ifdef DD_UNIQUE_PROFILE 20511 unique->uniqueLookUps++;
20514 if ((0x1ffffUL & (
unsigned long) unique->
cacheMisses) == 0) {
20520 if (index >= unique->
size) {
20525 level = unique->
perm[index];
20526 subtable = &(unique->
subtables[level]);
20535 previousP = &(nodelist[
pos]);
20536 looking = *previousP;
20538 while (T <
cuddT(looking)) {
20539 previousP = &(looking->
next);
20540 looking = *previousP;
20541 #ifdef DD_UNIQUE_PROFILE 20542 unique->uniqueLinks++;
20545 while (T ==
cuddT(looking) && E <
cuddE(looking)) {
20546 previousP = &(looking->
next);
20547 looking = *previousP;
20548 #ifdef DD_UNIQUE_PROFILE 20549 unique->uniqueLinks++;
20552 if (T ==
cuddT(looking) && E ==
cuddE(looking)) {
20553 if (looking->
ref == 0) {
20563 unsigned long cpuTime;
20566 if (retval != 0)
return(NULL);
20568 if (retval != 0)
return(NULL);
20583 if (retval != 0) unique->
reordered = 2;
20585 if (retval != 0) unique->
reordered = 2;
20594 (subtable->
dead > subtable->
keys * 0.95)))) {
20608 previousP = &(nodelist[
pos]);
20609 looking = *previousP;
20611 while (T <
cuddT(looking)) {
20612 previousP = &(looking->
next);
20613 looking = *previousP;
20614 #ifdef DD_UNIQUE_PROFILE 20615 unique->uniqueLinks++;
20618 while (T ==
cuddT(looking) && E <
cuddE(looking)) {
20619 previousP = &(looking->
next);
20620 looking = *previousP;
20621 #ifdef DD_UNIQUE_PROFILE 20622 unique->uniqueLinks++;
20629 if (looking == NULL) {
20639 previousP = &(nodelist[
pos]);
20640 looking2 = *previousP;
20642 while (T <
cuddT(looking2)) {
20643 previousP = &(looking2->
next);
20644 looking2 = *previousP;
20645 #ifdef DD_UNIQUE_PROFILE 20646 unique->uniqueLinks++;
20649 while (T ==
cuddT(looking2) && E <
cuddE(looking2)) {
20650 previousP = &(looking2->
next);
20651 looking2 = *previousP;
20652 #ifdef DD_UNIQUE_PROFILE 20653 unique->uniqueLinks++;
20657 looking->
index = index;
20658 cuddT(looking) = T;
20659 cuddE(looking) = E;
20660 looking->
next = *previousP;
20661 *previousP = looking;
20666 cuddCheckCollisionOrdering(unique,level,pos);
20737 unsigned int level;
20743 #ifdef DD_UNIQUE_PROFILE 20744 unique->uniqueLookUps++;
20747 if (index >= unique->
sizeZ) {
20751 level = unique->
permZ[index];
20752 subtable = &(unique->
subtableZ[level]);
20761 (10 * subtable->
dead > 9 * subtable->
keys))) {
20770 looking = nodelist[
pos];
20772 while (looking != NULL) {
20773 if (
cuddT(looking) == T &&
cuddE(looking) == E) {
20774 if (looking->
ref == 0) {
20779 looking = looking->
next;
20780 #ifdef DD_UNIQUE_PROFILE 20781 unique->uniqueLinks++;
20790 if (retval != 0)
return(NULL);
20792 if (retval != 0)
return(NULL);
20795 if (retval == 0) unique->
reordered = 2;
20798 if (retval != 0) unique->
reordered = 2;
20800 if (retval != 0) unique->
reordered = 2;
20809 if (looking == NULL)
return(NULL);
20810 looking->
index = index;
20811 cuddT(looking) = T;
20812 cuddE(looking) = E;
20813 looking->
next = nodelist[
pos];
20814 nodelist[
pos] = looking;
20846 #ifdef DD_UNIQUE_PROFILE 20847 unique->uniqueLookUps++;
20864 split.
value = value;
20868 looking = nodelist[
pos];
20875 while (looking != NULL) {
20878 if (looking->
ref == 0) {
20883 looking = looking->
next;
20884 #ifdef DD_UNIQUE_PROFILE 20885 unique->uniqueLinks++;
20893 if (looking == NULL)
return(NULL);
20896 looking->
next = nodelist[
pos];
20897 nodelist[
pos] = looking;
20921 unsigned int slots, oldslots;
20922 int shift, oldshift;
20936 (void) fprintf(unique->
err,
"minDead = %d\n", unique->
minDead);
20945 (void) fprintf(unique->
err,
"minDead = %d\n", unique->
minDead);
20957 slots = oldslots << 1;
20958 shift = oldshift - 1;
20963 MMoutOfMemory = saveHandler;
20964 if (nodelist == NULL) {
20965 (void) fprintf(unique->
err,
20966 "Unable to resize subtable %d for lack of memory\n",
20970 if (unique->
stash != NULL) {
20972 unique->
stash = NULL;
20988 for (j = 0; (unsigned) j < oldslots; j++) {
20990 node = oldnodelist[j];
20991 evenP = &(nodelist[j<<1]);
20992 oddP = &(nodelist[(j<<1)+1]);
20993 while (node != sentinel) {
20998 oddP = &(node->
next);
21001 evenP = &(node->
next);
21005 *evenP = *oddP = sentinel;
21010 (void) fprintf(unique->
err,
21011 "rehashing layer %d: keys %d dead %d new size %d\n",
21025 slots = oldslots << 1;
21026 shift = oldshift - 1;
21030 MMoutOfMemory = saveHandler;
21031 if (nodelist == NULL) {
21032 (void) fprintf(unique->
err,
21033 "Unable to resize constant subtable for lack of memory\n");
21035 for (j = 0; j < unique->
size; j++) {
21045 for (j = 0; (unsigned) j < slots; j++) {
21046 nodelist[j] = NULL;
21048 for (j = 0; (unsigned) j < oldslots; j++) {
21049 node = oldnodelist[j];
21050 while (node != NULL) {
21055 nodelist[
pos] = node;
21062 (void) fprintf(unique->
err,
21063 "rehashing constants: keys %d dead %d new size %d\n",
21071 unique->
slots += (slots - oldslots);
21099 int oldsize,newsize;
21100 int i,j,reorderSave;
21101 unsigned int numSlots = unique->
initSlots;
21102 int *newperm, *newinvperm;
21104 oldsize = unique->
sizeZ;
21106 if (index < unique->maxSizeZ) {
21107 for (i = oldsize; i <= index; i++) {
21114 unique->
permZ[i] = i;
21118 if (newnodelist == NULL) {
21122 for (j = 0; (unsigned) j < numSlots; j++) {
21123 newnodelist[j] = NULL;
21133 (void) fprintf(unique->
err,
21134 "Increasing the ZDD table size from %d to %d\n",
21138 if (newsubtables == NULL) {
21142 newperm =
ALLOC(
int,newsize);
21143 if (newperm == NULL) {
21147 newinvperm =
ALLOC(
int,newsize);
21148 if (newinvperm == NULL) {
21154 if (newsize > unique->
maxSize) {
21157 if (unique->
stack == NULL) {
21161 unique->
stack[0] = NULL;
21166 for (i = 0; i < oldsize; i++) {
21173 newperm[i] = unique->
permZ[i];
21174 newinvperm[i] = unique->
invpermZ[i];
21176 for (i = oldsize; i <= index; i++) {
21177 newsubtables[i].
slots = numSlots;
21178 newsubtables[i].
shift =
sizeof(int) * 8 -
21180 newsubtables[i].
keys = 0;
21182 newsubtables[i].
dead = 0;
21186 if (newnodelist == NULL) {
21190 for (j = 0; (unsigned) j < numSlots; j++) {
21191 newnodelist[j] = NULL;
21198 unique->
permZ = newperm;
21202 unique->
slots += (index + 1 - unique->
sizeZ) * numSlots;
21204 unique->
sizeZ = index + 1;
21244 for (i = 0; i < unique->
size; i++) {
21250 (void) fprintf(unique->
err,
"Slowing down table growth: ");
21251 (void) fprintf(unique->
err,
"GC fraction = %.2f\t", unique->
gcFrac);
21252 (void) fprintf(unique->
err,
"minDead = %u\n", unique->
minDead);
21278 unsigned int slots, oldslots;
21279 int shift, oldshift;
21290 (void) fprintf(unique->
err,
"GC fraction = %.2f\t",
21292 (void) fprintf(unique->
err,
"minDead = %d\n", unique->
minDead);
21311 }
while (slots * DD_MAX_SUBTABLE_DENSITY < unique->subtableZ[i].keys);
21316 MMoutOfMemory = saveHandler;
21317 if (nodelist == NULL) {
21318 (void) fprintf(unique->
err,
21319 "Unable to resize ZDD subtable %d for lack of memory.\n",
21322 for (j = 0; j < unique->
sizeZ; j++) {
21331 for (j = 0; (unsigned) j < slots; j++) {
21332 nodelist[j] = NULL;
21334 for (j = 0; (unsigned) j < oldslots; j++) {
21335 node = oldnodelist[j];
21336 while (node != NULL) {
21340 nodelist[
pos] = node;
21347 (void) fprintf(unique->
err,
21348 "rehashing layer %d: keys %d dead %d new size %d\n",
21355 unique->
slots += (slots - oldslots);
21387 int oldsize,newsize;
21388 int i,j,reorderSave;
21390 int *newperm, *newinvperm, *newmap;
21393 oldsize = unique->
size;
21395 if (index >= 0 && index < unique->maxSize) {
21396 for (i = oldsize; i <= index; i++) {
21409 unique->
perm[i] = i;
21413 if (newnodelist == NULL) {
21414 for (j = oldsize; j < i; j++) {
21420 for (j = 0; j < numSlots; j++) {
21421 newnodelist[j] = sentinel;
21424 if (unique->
map != NULL) {
21425 for (i = oldsize; i <= index; i++) {
21426 unique->
map[i] = i;
21434 newsize = (index < 0) ? amount : index + amount;
21436 (void) fprintf(unique->
err,
21437 "Increasing the table size from %d to %d\n",
21441 if (newsubtables == NULL) {
21446 if (newvars == NULL) {
21447 FREE(newsubtables);
21451 newperm =
ALLOC(
int,newsize);
21452 if (newperm == NULL) {
21453 FREE(newsubtables);
21458 newinvperm =
ALLOC(
int,newsize);
21459 if (newinvperm == NULL) {
21460 FREE(newsubtables);
21466 if (unique->
map != NULL) {
21467 newmap =
ALLOC(
int,newsize);
21468 if (newmap == NULL) {
21469 FREE(newsubtables);
21478 unique->
memused += (newsize - unique->
maxSize) * ((numSlots+1) *
21483 if (unique->
stack == NULL) {
21484 FREE(newsubtables);
21488 if (unique->
map != NULL) {
21494 unique->
stack[0] = NULL;
21499 for (i = 0; i < oldsize; i++) {
21512 newvars[i] = unique->
vars[i];
21513 newperm[i] = unique->
perm[i];
21514 newinvperm[i] = unique->
invperm[i];
21516 for (i = oldsize; i <= index; i++) {
21517 newsubtables[i].
slots = numSlots;
21518 newsubtables[i].
shift =
sizeof(int) * 8 -
21520 newsubtables[i].
keys = 0;
21522 newsubtables[i].
dead = 0;
21532 if (newnodelist == NULL) {
21536 for (j = 0; j < numSlots; j++) {
21537 newnodelist[j] = sentinel;
21540 if (unique->
map != NULL) {
21541 for (i = 0; i < oldsize; i++) {
21542 newmap[i] = unique->
map[i];
21544 for (i = oldsize; i <= index; i++) {
21548 unique->
map = newmap;
21554 unique->
vars = newvars;
21556 unique->
perm = newperm;
21558 unique->
invperm = newinvperm;
21569 unique->
size = index + 1;
21570 if (unique->
tree != NULL) {
21573 unique->
slots += (index + 1 - oldsize) * numSlots;
21576 reorderSave = unique->
autoDyn;
21578 for (i = oldsize; i <= index; i++) {
21580 if (unique->
vars[i] == NULL) {
21581 unique->
autoDyn = reorderSave;
21582 for (j = oldsize; j < i; j++) {
21585 unique->
vars[j] = NULL;
21587 for (j = oldsize; j <= index; j++) {
21591 unique->
size = oldsize;
21592 unique->
slots -= (index + 1 - oldsize) * numSlots;
21598 unique->
autoDyn = reorderSave;
21638 #ifndef DD_UNSORTED_FREE_LIST 21639 #ifdef DD_RED_BLACK_FREE_LIST 21663 while ((scan = *scanP) != NULL) {
21664 stack[stackN++] = scanP;
21665 if (DD_INSERT_COMPARE(node, scan) == 0) {
21666 DD_NEXT(node) = DD_NEXT(scan);
21667 DD_NEXT(scan) = node;
21670 scanP = (node < scan) ? &DD_LEFT(scan) : &DD_RIGHT(scan);
21672 DD_RIGHT(node) = DD_LEFT(node) = DD_NEXT(node) = NULL;
21673 DD_COLOR(node) = DD_RED;
21675 stack[stackN] = &node;
21676 cuddDoRebalance(stack,stackN);
21706 DdNode *current, *next, *prev, *end;
21715 while (current != NULL) {
21716 if (DD_RIGHT(current) != NULL) {
21724 next = DD_RIGHT(current);
21725 DD_RIGHT(current) = NULL;
21737 for (end = current; DD_NEXT(end) != NULL; end = DD_NEXT(end));
21738 DD_NEXT(end) = list;
21743 if (DD_LEFT(current) != NULL) {
21744 next = DD_LEFT(current);
21775 DdNode *oldRoot = *nodeP;
21777 *nodeP = newRoot = DD_RIGHT(oldRoot);
21778 DD_RIGHT(oldRoot) = DD_LEFT(newRoot);
21779 DD_LEFT(newRoot) = oldRoot;
21801 DdNode *oldRoot = *nodeP;
21803 *nodeP = newRoot = DD_LEFT(oldRoot);
21804 DD_LEFT(oldRoot) = DD_RIGHT(newRoot);
21805 DD_RIGHT(newRoot) = oldRoot;
21827 DdNode *x, *y, *parent, *grandpa;
21829 xP = stack[stackN];
21832 while (--stackN >= 0) {
21833 parentP = stack[stackN];
21835 if (DD_IS_BLACK(parent))
break;
21837 grandpaP = stack[stackN-1];
21838 grandpa = *grandpaP;
21839 if (parent == DD_LEFT(grandpa)) {
21840 y = DD_RIGHT(grandpa);
21841 if (y != NULL && DD_IS_RED(y)) {
21842 DD_COLOR(parent) = DD_BLACK;
21843 DD_COLOR(y) = DD_BLACK;
21844 DD_COLOR(grandpa) = DD_RED;
21848 if (x == DD_RIGHT(parent)) {
21849 cuddRotateLeft(parentP);
21850 DD_COLOR(x) = DD_BLACK;
21852 DD_COLOR(parent) = DD_BLACK;
21854 DD_COLOR(grandpa) = DD_RED;
21855 cuddRotateRight(grandpaP);
21859 y = DD_LEFT(grandpa);
21860 if (y != NULL && DD_IS_RED(y)) {
21861 DD_COLOR(parent) = DD_BLACK;
21862 DD_COLOR(y) = DD_BLACK;
21863 DD_COLOR(grandpa) = DD_RED;
21867 if (x == DD_LEFT(parent)) {
21868 cuddRotateRight(parentP);
21869 DD_COLOR(x) = DD_BLACK;
21871 DD_COLOR(parent) = DD_BLACK;
21873 DD_COLOR(grandpa) = DD_RED;
21874 cuddRotateLeft(grandpaP);
21878 DD_COLOR(*(stack[0])) = DD_BLACK;
21905 while (auxnode != NULL) {
21907 if (auxnode->
child != NULL) {
21931 cuddCheckCollisionOrdering(
21943 node = nodelist[j];
21944 if (node == sentinel)
return(1);
21946 while (next != sentinel) {
21949 (void) fprintf(unique->
err,
21950 "Unordered list: index %u, position %d\n", i, j);
21979 const char *caller )
21982 (void) fprintf(unique->
err,
21983 "%s: problem in constants\n", caller);
21984 }
else if (i != -1) {
21985 (void) fprintf(unique->
err,
21986 "%s: problem in table %d\n", caller, i);
21988 (void) fprintf(unique->
err,
" dead count != deleted\n");
21989 (void) fprintf(unique->
err,
" This problem is often due to a missing \ 21990 call to Cudd_Ref\n or to an extra call to Cudd_RecursiveDeref.\n \ 21991 See the CUDD Programmer's Guide for additional details.");
22113 #define MODULUS1 2147483563 22114 #define LEQA1 40014 22115 #define LEQQ1 53668 22116 #define LEQR1 12211 22117 #define MODULUS2 2147483399 22118 #define LEQA2 40692 22119 #define LEQQ2 52774 22121 #define STAB_SIZE 64 22122 #define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE) 22152 #define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ') 22222 max = pow(2.0,(
double)nvars);
22224 if (table == NULL) {
22274 DdNode *top, *treg, *next, *nreg, *prev, *preg;
22279 if (dd == NULL || f == NULL)
return(NULL);
22294 gen->
stack.stack = NULL;
22299 if (gen->
gen.
cubes.cube == NULL) {
22304 for (i = 0; i < nvars; i++) gen->
gen.
cubes.cube[i] = 2;
22311 if (gen->
stack.stack == NULL) {
22317 for (i = 0; i <= nvars; i++) gen->
stack.stack[i] = NULL;
22328 next =
cuddE(treg);
22329 if (top != treg) next =
Cudd_Not(next);
22334 if (gen->
stack.sp == 1) {
22342 nreg =
cuddT(preg);
22343 if (prev != preg) {next =
Cudd_Not(nreg);}
else {next = nreg;}
22391 DdNode *top, *treg, *next, *nreg, *prev, *preg;
22396 if (gen->
stack.sp == 1) {
22406 nreg =
cuddT(preg);
22407 if (prev != preg) {next =
Cudd_Not(nreg);}
else {next = nreg;}
22424 next =
cuddE(treg);
22425 if (top != treg) next =
Cudd_Not(next);
22430 if (gen->
stack.sp == 1) {
22438 nreg =
cuddT(preg);
22439 if (prev != preg) {next =
Cudd_Not(nreg);}
else {next = nreg;}
22504 DdNode *implicant, *prime, *tmp;
22508 if (dd == NULL || l == NULL || u == NULL)
return(NULL);
22523 gen->
stack.stack = NULL;
22538 if (implicant == NULL) {
22546 if (prime == NULL) {
22603 DdNode *implicant, *prime, *tmp;
22611 if (implicant == NULL) {
22617 if (prime == NULL) {
22679 for (i = size-1; i >= 0; i--) {
22689 }
else if (e == zero) {
22696 if (scan == zero) {
22732 if (dd == NULL || f == NULL)
return(NULL);
22749 if (gen->
stack.stack == NULL) {
22817 if (gen == NULL)
return(0);
22818 switch (gen->
type) {
22857 if (gen == NULL)
return(1);
22985 (void) fflush(stdout);
22986 (void) fprintf(stderr,
"\nunable to allocate %ld bytes\n", size);
23043 if (retval != 1)
return(retval);
23076 if (table == NULL) {
23119 #if SIZEOF_VOID_P == 8 23120 (void) fprintf(dd->
out,
"ID = %c0x%lx\tvalue = %-9g\n",
bang(f),
23123 (void) fprintf(dd->
out,
"ID = %c0x%x\tvalue = %-9g\n",
bang(f),
23134 #if SIZEOF_VOID_P == 8 23135 (void) fprintf(dd->
out,
"ID = %c0x%lx\tindex = %d\tr = %d\t",
bang(f),
23138 (void) fprintf(dd->
out,
"ID = %c0x%x\tindex = %d\tr = %d\t",
bang(f),
23142 #if SIZEOF_VOID_P == 8 23143 (void) fprintf(dd->
out,
"ID = %c0x%lx\tindex = %u\t",
bang(f),
23146 (void) fprintf(dd->
out,
"ID = %c0x%x\tindex = %hu\t",
bang(f),
23152 (void) fprintf(dd->
out,
"T = %-9g\t",
cuddV(n));
23155 #if SIZEOF_VOID_P == 8 23166 (void) fprintf(dd->
out,
"E = %c%-9g\n",
bang(n),
cuddV(N));
23169 #if SIZEOF_VOID_P == 8 23177 if (
dp2(dd,N,t) == 0)
23214 if (node != background && node != zero) {
23215 for (i = 0; i < dd->
size; i++) {
23217 if (v == 0) (void) fprintf(dd->
out,
"0");
23218 else if (v == 1) (void) fprintf(dd->
out,
"1");
23219 else (
void) fprintf(dd->
out,
"-");
23221 (void) fprintf(dd->
out,
" % g\n",
cuddV(node));
23267 return(1 + tval + eval);
23293 int tindex, eindex;
23307 return(eindex + 1);
23336 int tval, eval, val;
23340 if (!
st_lookup(table,(
char *)node,(
char **)ptr)) {
23355 if ((
int) node->
index == i) {
23357 *ptr =
cuddT(node);
23360 *ptr =
cuddE(node);
23363 if (node->
ref > 1) {
23374 if (node->
ref > 1) {
23379 val = 1 + tval + eval;
23386 if (ptrT == ptrE) {
23389 if (node->
ref > 1) {
23394 }
else if ((ptrT !=
cuddT(node) || ptrE !=
cuddE(node)) &&
23399 val = 1 + tval + eval;
23401 if (node->
ref > 1) {
23408 val = 1 + tval + eval;
23435 unsigned int level;
23440 if (index >= unique->
size) {
23444 level = unique->
perm[index];
23445 subtable = &(unique->
subtables[level]);
23454 looking = nodelist[posn];
23456 while (T <
cuddT(looking)) {
23459 while (T ==
cuddT(looking) && E <
cuddE(looking)) {
23462 if (
cuddT(looking) == T &&
cuddE(looking) == E) {
23501 if ((
int) node->
index == i)
return(tval);
23503 return(1 + tval + eval);
23533 double min, minT, minE;
23539 if (node == background || node == zero) {
23547 if (res->
ref == 0) {
23560 if (minT == (
double)
CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23563 if (minE == (
double)CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23573 return((
double)CUDD_OUT_OF_MEM);
23606 double paths, *ppaths, paths1, paths2;
23621 if (paths1 == (
double)
CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23623 if (paths2 == (
double)CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23624 paths = paths1 + paths2;
23626 ppaths =
ALLOC(
double,1);
23627 if (ppaths == NULL) {
23628 return((
double)CUDD_OUT_OF_MEM);
23635 return((
double)CUDD_OUT_OF_MEM);
23674 if (node == background || node == zero) {
23700 if (node->
ref > 1) {
23739 double paths, *ppaths, paths1, paths2;
23757 if (paths1 == (
double)
CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23759 if (paths2 == (
double)CUDD_OUT_OF_MEM)
return((
double)CUDD_OUT_OF_MEM);
23760 paths = paths1 + paths2;
23762 ppaths =
ALLOC(
double,1);
23763 if (ppaths == NULL) {
23764 return((
double)CUDD_OUT_OF_MEM);
23771 return((
double)CUDD_OUT_OF_MEM);
23799 support[f->
index] = 1;
23866 return(tval + eval);
23896 if (
string == NULL || node == NULL)
return(0);
23901 if (nminterms == 0 || node == bzero)
return(1);
23915 if (min2 == (
double)CUDD_OUT_OF_MEM)
return(0);
23917 t = (int)((
double)nminterms * min1 / (min1 + min2) + 0.5);
23918 for (i = 0; i < t; i++)
23919 string[i][N->
index] =
'1';
23920 for (i = t; i < nminterms; i++)
23921 string[i][N->
index] =
'0';
23966 var = dd->
vars[index];
24074 extern int ddTotalNISwaps;
24135 switch (submethod) {
24153 if (table->
keys - table->
isolated != (
unsigned) supposedOpt) {
24154 (void) fprintf(table->
err,
"Convergence failed! (%d != %d)\n",
24164 if (table->
keys - table->
isolated != (
unsigned) supposedOpt) {
24165 (void) fprintf(table->
err,
"Convergence failed! (%d != %d)\n",
24170 default:
return(0);
24206 assert(low >= 0 && high < table->size);
24209 if (high-low < 1)
return(0);
24212 for (x = low; x < high; x++) {
24215 if (res == 0)
return(0);
24218 if (res == 0)
return(0);
24222 (void) fprintf(table->
out,
"-");
24224 (void) fprintf(table->
out,
"=");
24226 fflush(table->
out);
24262 assert(low >= 0 && high < table->size);
24268 events =
ALLOC(
int,nwin);
24269 if (events == NULL) {
24273 for (x=0; x<nwin; x++) {
24280 for (x=0; x<nwin; x++) {
24296 if (x < nwin-1) events[x+1] = 1;
24297 if (x > 0) events[x-1] = 1;
24303 (void) fprintf(table->
out,
"-");
24305 (void) fprintf(table->
out,
"=");
24307 fflush(table->
out);
24313 (void) fprintf(table->
out,
"|");
24314 fflush(table->
out);
24317 }
while (newevent);
24367 if (sizeNew < size) {
24368 if (sizeNew == 0)
return(0);
24374 if (sizeNew < size) {
24375 if (sizeNew == 0)
return(0);
24381 if (sizeNew < size) {
24382 if (sizeNew == 0)
return(0);
24388 if (sizeNew < size) {
24389 if (sizeNew == 0)
return(0);
24395 if (sizeNew < size) {
24396 if (sizeNew == 0)
return(0);
24412 default:
return(0);
24447 assert(low >= 0 && high < table->size);
24450 if (high-low < 2)
return(
ddWindow2(table,low,high));
24452 for (x = low; x+1 < high; x++) {
24454 if (res == 0)
return(0);
24457 (void) fprintf(table->
out,
"=");
24459 (void) fprintf(table->
out,
"-");
24461 fflush(table->
out);
24496 assert(low >= 0 && high < table->size);
24502 events =
ALLOC(
int,nwin);
24503 if (events == NULL) {
24507 for (x=0; x<nwin; x++) {
24513 for (x=0; x<nwin; x++) {
24520 if (x < nwin-1) events[x+1] = 1;
24521 if (x > 1) events[x-2] = 1;
24527 if (x < nwin-2) events[x+2] = 1;
24528 if (x < nwin-1) events[x+1] = 1;
24529 if (x > 0) events[x-1] = 1;
24530 if (x > 1) events[x-2] = 1;
24534 if (x < nwin-2) events[x+2] = 1;
24535 if (x > 0) events[x-1] = 1;
24545 (void) fprintf(table->
out,
"=");
24547 (void) fprintf(table->
out,
"-");
24549 fflush(table->
out);
24555 (void) fprintf(table->
out,
"|");
24556 fflush(table->
out);
24559 }
while (newevent);
24596 x = w+1; y = x+1; z = y+1;
24616 if (sizeNew < size) {
24617 if (sizeNew == 0)
return(0);
24623 if (sizeNew < size) {
24624 if (sizeNew == 0)
return(0);
24630 if (sizeNew < size || (sizeNew == size &&
ABDC < best)) {
24631 if (sizeNew == 0)
return(0);
24637 if (sizeNew < size) {
24638 if (sizeNew == 0)
return(0);
24644 if (sizeNew < size || (sizeNew == size &&
ADCB < best)) {
24645 if (sizeNew == 0)
return(0);
24651 if (sizeNew < size) {
24652 if (sizeNew == 0)
return(0);
24658 if (sizeNew < size) {
24659 if (sizeNew == 0)
return(0);
24665 if (sizeNew < size) {
24666 if (sizeNew == 0)
return(0);
24672 if (sizeNew < size || (sizeNew == size &&
BDAC < best)) {
24673 if (sizeNew == 0)
return(0);
24679 if (sizeNew < size || (sizeNew == size &&
BDCA < best)) {
24680 if (sizeNew == 0)
return(0);
24686 if (sizeNew < size) {
24687 if (sizeNew == 0)
return(0);
24693 if (sizeNew < size || (sizeNew == size &&
DCBA < best)) {
24694 if (sizeNew == 0)
return(0);
24700 if (sizeNew < size || (sizeNew == size &&
DCAB < best)) {
24701 if (sizeNew == 0)
return(0);
24707 if (sizeNew < size || (sizeNew == size &&
CDAB < best)) {
24708 if (sizeNew == 0)
return(0);
24714 if (sizeNew < size || (sizeNew == size &&
CDBA < best)) {
24715 if (sizeNew == 0)
return(0);
24721 if (sizeNew < size || (sizeNew == size &&
CBDA < best)) {
24722 if (sizeNew == 0)
return(0);
24728 if (sizeNew < size || (sizeNew == size &&
BCDA < best)) {
24729 if (sizeNew == 0)
return(0);
24735 if (sizeNew < size || (sizeNew == size &&
BCAD < best)) {
24736 if (sizeNew == 0)
return(0);
24742 if (sizeNew < size || (sizeNew == size &&
CBAD < best)) {
24743 if (sizeNew == 0)
return(0);
24749 if (sizeNew < size || (sizeNew == size &&
CABD < best)) {
24750 if (sizeNew == 0)
return(0);
24756 if (sizeNew < size || (sizeNew == size &&
CADB < best)) {
24757 if (sizeNew == 0)
return(0);
24763 if (sizeNew < size || (sizeNew == size &&
ACDB < best)) {
24764 if (sizeNew == 0)
return(0);
24770 if (sizeNew < size || (sizeNew == size &&
ACBD < best)) {
24771 if (sizeNew == 0)
return(0);
24813 default:
return(0);
24848 assert(low >= 0 && high < table->size);
24851 if (high-low < 3)
return(
ddWindow3(table,low,high));
24853 for (w = low; w+2 < high; w++) {
24855 if (res == 0)
return(0);
24858 (void) fprintf(table->
out,
"=");
24860 (void) fprintf(table->
out,
"-");
24862 fflush(table->
out);
24897 assert(low >= 0 && high < table->size);
24903 events =
ALLOC(
int,nwin);
24904 if (events == NULL) {
24908 for (x=0; x<nwin; x++) {
24914 for (x=0; x<nwin; x++) {
24921 if (x < nwin-1) events[x+1] = 1;
24922 if (x > 2) events[x-3] = 1;
24926 if (x < nwin-3) events[x+3] = 1;
24927 if (x < nwin-1) events[x+1] = 1;
24928 if (x > 0) events[x-1] = 1;
24929 if (x > 2) events[x-3] = 1;
24933 if (x < nwin-3) events[x+3] = 1;
24934 if (x > 0) events[x-1] = 1;
24940 if (x < nwin-3) events[x+3] = 1;
24941 if (x < nwin-2) events[x+2] = 1;
24942 if (x > 0) events[x-1] = 1;
24943 if (x > 1) events[x-2] = 1;
24959 if (x < nwin-3) events[x+3] = 1;
24960 if (x < nwin-2) events[x+2] = 1;
24961 if (x < nwin-1) events[x+1] = 1;
24962 if (x > 0) events[x-1] = 1;
24963 if (x > 1) events[x-2] = 1;
24964 if (x > 2) events[x-3] = 1;
24970 if (x < nwin-2) events[x+2] = 1;
24971 if (x < nwin-1) events[x+1] = 1;
24972 if (x > 1) events[x-2] = 1;
24973 if (x > 2) events[x-3] = 1;
24977 if (x < nwin-2) events[x+2] = 1;
24978 if (x > 1) events[x-2] = 1;
24988 (void) fprintf(table->
out,
"=");
24990 (void) fprintf(table->
out,
"-");
24992 fflush(table->
out);
24998 (void) fprintf(table->
out,
"|");
24999 fflush(table->
out);
25002 }
while (newevent);
25152 int v, top_f, top_g;
25153 DdNode *tmp, *term1, *term2, *term3;
25154 DdNode *f0, *f1, *fd, *g0, *g1, *gd;
25155 DdNode *R0, *R1, *Rd, *N0, *N1;
25163 if (f == zero || g == zero)
25214 if (term1 == NULL) {
25226 if (term2 == NULL) {
25239 if (term3 == NULL) {
25298 if (term1 == NULL) {
25308 if (term2 == NULL) {
25319 if (term3 == NULL) {
25389 int v, top_f, top_g;
25390 DdNode *term1, *term2, *term3, *term4;
25392 DdNode *f0, *f1, *g0, *g1;
25399 if (f == zero || g == zero)
25433 if (term1 == NULL) {
25442 if (term2 == NULL) {
25452 if (term3 == NULL) {
25463 if (term4 == NULL) {
25479 if (sum1 == NULL) {
25490 if (sum2 == NULL) {
25536 DdNode *f0, *f1, *fd, *g0, *g1, *gd;
25544 if (f == zero || f == one)
25694 int v, top_f, top_g, vf, vg;
25697 DdNode *f0, *f1, *fd, *g0, *g1, *gd;
25700 DdNode *term1, *term0, *termd;
25707 if (f == zero || f == one)
25721 v =
ddMin(top_f, top_g);
25723 if (v == top_f && vf < vg) {
25736 if (term1 == NULL) {
25745 if (term0 == NULL) {
25754 if (termd == NULL) {
25934 DdNode *f0, *f1, *g0, *g1;
25941 if (f == zero || f == one)
25977 if (r != zero && g0 != zero) {
26034 DdNode *f0, *f1, *g0, *g1;
26041 if (f == zero || f == one)
26077 if (r != zero && g0 != zero) {
26137 int top, hv, ht, pv, nv;
26141 level = dd->
permZ[v];
26293 DdNode *b, *isop, *zdd_I;
26336 int pv = (index >> 1) << 1;
26357 int nv = index | 0x1;
26379 return(dd->
permZ[pv]);
26400 return(dd->
permZ[nv]);
26495 static int extsymmcalls;
26496 static int extsymm;
26497 static int secdiffcalls;
26498 static int secdiff;
26499 static int secdiffmisfire;
26518 static int zddCountInternalMtrNodes (
DdManager *table,
MtrNode *treenode);
26571 tempTree = table->
treeZ == NULL;
26576 nvars = table->
sizeZ;
26579 if (pr > 0 && !tempTree)
26580 (void) fprintf(table->
out,
"cuddZddTreeSifting:");
26586 (void) fprintf(table->
out,
"\n");
26589 for (i = 0; i < table->
size; i++) {
26590 (void) fprintf(table->
out,
"%s%d",
26591 (i == 0) ?
"" :
",", table->
invperm[i]);
26593 (void) fprintf(table->
out,
"\n");
26594 for (i = 0; i < table->
size; i++) {
26595 (void) fprintf(table->
out,
"%s%d",
26596 (i == 0) ?
"" :
",", table->
perm[i]);
26598 (void) fprintf(table->
out,
"\n\n");
26601 for (i = 0; i < table->
sizeZ; i++) {
26602 (void) fprintf(table->
out,
"%s%d",
26603 (i == 0) ?
"" :
",", table->
invpermZ[i]);
26605 (void) fprintf(table->
out,
"\n");
26606 for (i = 0; i < table->
sizeZ; i++) {
26607 (void) fprintf(table->
out,
"%s%d",
26608 (i == 0) ?
"" :
",", table->
permZ[i]);
26610 (void) fprintf(table->
out,
"\n");
26619 secdiffmisfire = 0;
26621 (void) fprintf(table->
out,
"\n");
26623 (void) fprintf(table->
out,
"#:IM_NODES %8d: group tree nodes\n",
26624 zddCountInternalMtrNodes(table,table->
treeZ));
26631 for (i = 0; i < nvars; i++)
26641 (void) fprintf(table->
out,
"\nextsymmcalls = %d\n",extsymmcalls);
26642 (void) fprintf(table->
out,
"extsymm = %d",extsymm);
26646 (void) fprintf(table->
out,
"\nsecdiffcalls = %d\n",secdiffcalls);
26647 (void) fprintf(table->
out,
"secdiff = %d\n",secdiff);
26648 (void) fprintf(table->
out,
"secdiffmisfire = %d",secdiffmisfire);
26687 auxnode = treenode;
26688 while (auxnode != NULL) {
26689 if (auxnode->
child != NULL) {
26695 }
else if (auxnode->
size > 1) {
26719 zddCountInternalMtrNodes(
26724 int count,nodeCount;
26728 auxnode = treenode;
26729 while (auxnode != NULL) {
26732 count = zddCountInternalMtrNodes(table,auxnode->
child);
26733 nodeCount += count;
26767 unsigned int initialSize;
26778 (void) fprintf(table->
out,
" ");
26790 initialSize = table->
keysZ;
26792 if (initialSize <= table->keysZ)
26796 (
void) fprintf(table->
out,
"\n");
26798 }
while (result != 0);
26814 initialSize = table->
keysZ;
26816 if (initialSize <= table->keysZ)
26820 (
void) fprintf(table->
out,
"\n");
26822 }
while (result != 0);
26836 if (pr > 0) (void) fprintf(table->
out,
"zddReorderChildren:");
26873 if ((
int) treenode->
low >= table->
sizeZ) {
26874 *lower = table->
sizeZ;
26879 *lower = low = (
unsigned int) table->
permZ[treenode->
index];
26880 high = (
int) (low + treenode->
size - 1);
26882 if (high >= table->
sizeZ) {
26891 if (auxnode == NULL) {
26892 *upper = (
unsigned int) table->
sizeZ - 1;
26899 while (auxnode != NULL) {
26900 int thisLower = table->
permZ[auxnode->
low];
26901 int thisUpper = thisLower + auxnode->
size - 1;
26902 if (thisUpper >= table->
sizeZ && thisLower < table->sizeZ)
26903 *upper = (
unsigned int) thisLower - 1;
26909 *upper = (
unsigned int) high;
26914 assert(treenode->
size >= *upper - *lower + 1);
26941 return((*ptrX) - (*ptrY));
26975 unsigned previousSize;
26979 nvars = table->
sizeZ;
26984 var =
ALLOC(
int,nvars);
26987 goto zddGroupSiftingOutOfMem;
26990 if (
entry == NULL) {
26992 goto zddGroupSiftingOutOfMem;
26994 sifted =
ALLOC(
int,nvars);
26995 if (sifted == NULL) {
26997 goto zddGroupSiftingOutOfMem;
27001 for (i = 0, classes = 0; i < nvars; i++) {
27003 x = table->
permZ[i];
27022 if (sifted[xindex] == 1)
27024 x = table->
permZ[xindex];
27025 if (x < lower || x > upper)
27028 previousSize = table->
keysZ;
27035 if (!result)
goto zddGroupSiftingOutOfMem;
27038 if (table->
keysZ < previousSize) {
27039 (void) fprintf(table->
out,
"-");
27040 }
else if (table->
keysZ > previousSize) {
27041 (void) fprintf(table->
out,
"+");
27043 (void) fprintf(table->
out,
"=");
27045 fflush(table->
out);
27049 x = table->
permZ[xindex];
27056 }
while (x != xInit);
27060 if (pr > 0) (void) fprintf(table->
out,
"zddGroupSifting:");
27070 zddGroupSiftingOutOfMem:
27072 if (var != NULL)
FREE(var);
27073 if (sifted != NULL)
FREE(sifted);
27109 if (pr > 0) (void) fprintf(table->
out,
"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
27113 initialSize = table->
keysZ;
27121 if (x == xHigh)
return(1);
27124 goto zddGroupSiftingAuxOutOfMem;
27132 if (!result)
goto zddGroupSiftingAuxOutOfMem;
27143 goto zddGroupSiftingAuxOutOfMem;
27151 if (!result)
goto zddGroupSiftingAuxOutOfMem;
27153 }
else if (x - xLow > xHigh - x) {
27155 goto zddGroupSiftingAuxOutOfMem;
27162 while ((
unsigned) x < table->subtableZ[x].next)
27167 assert((
unsigned) x <= table->subtableZ[x].next);
27171 goto zddGroupSiftingAuxOutOfMem;
27178 if (!result)
goto zddGroupSiftingAuxOutOfMem;
27185 goto zddGroupSiftingAuxOutOfMem;
27191 while ((
unsigned) x < table->subtableZ[x].next)
27199 goto zddGroupSiftingAuxOutOfMem;
27206 if (!result)
goto zddGroupSiftingAuxOutOfMem;
27209 while (moves != NULL) {
27210 move = moves->
next;
27217 zddGroupSiftingAuxOutOfMem:
27218 while (moves != NULL) {
27219 move = moves->
next;
27257 limitSize = table->
keysZ;
27260 while (x >= xLow) {
27270 if (size == 0)
goto zddGroupSiftingUpOutOfMem;
27272 if (move == NULL)
goto zddGroupSiftingUpOutOfMem;
27277 move->
next = *moves;
27281 if (pr > 0) (void) fprintf(table->
out,
"zddGroupSiftingUp (2 single groups):\n");
27283 if ((
double) size > (double) limitSize * table->
maxGrowth)
27285 if (size < limitSize) limitSize = size;
27288 if (size == 0)
goto zddGroupSiftingUpOutOfMem;
27289 if ((
double) size > (
double) limitSize * table->
maxGrowth)
27291 if (size < limitSize) limitSize = size;
27299 zddGroupSiftingUpOutOfMem:
27300 while (*moves != NULL) {
27301 move = (*moves)->
next;
27336 limitSize = size = table->
keysZ;
27338 while (y <= xHigh) {
27352 if (size == 0)
goto zddGroupSiftingDownOutOfMem;
27356 if (move == NULL)
goto zddGroupSiftingDownOutOfMem;
27361 move->
next = *moves;
27365 if (pr > 0) (void) fprintf(table->
out,
"zddGroupSiftingDown (2 single groups):\n");
27367 if ((
double) size > (double) limitSize * table->
maxGrowth)
27369 if (size < limitSize) limitSize = size;
27374 if (size == 0)
goto zddGroupSiftingDownOutOfMem;
27375 if ((
double) size > (
double) limitSize * table->
maxGrowth)
27377 if (size < limitSize) limitSize = size;
27385 zddGroupSiftingDownOutOfMem:
27386 while (*moves != NULL) {
27387 move = (*moves)->
next;
27416 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
27418 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 27419 int initialSize,bestSize;
27429 xsize = xbot - xtop + 1;
27431 while ((
unsigned) ybot < table->subtableZ[ybot].next)
27434 ysize = ybot - ytop + 1;
27436 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 27437 initialSize = bestSize = table->
keysZ;
27440 for (i = 1; i <= ysize; i++) {
27441 for (j = 1; j <= xsize; j++) {
27443 if (size == 0)
goto zddGroupMoveOutOfMem;
27444 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 27445 if (size < bestSize)
27448 swapx = x; swapy = y;
27455 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 27456 if ((bestSize < initialSize) && (bestSize < size))
27457 (void) fprintf(table->
out,
"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size);
27462 for (i = 0; i < ysize - 1; i++) {
27470 for (i = 0; i < xsize - 1; i++) {
27477 if (pr > 0) (void) fprintf(table->
out,
"zddGroupMove:\n");
27482 if (move == NULL)
goto zddGroupMoveOutOfMem;
27487 move->
next = *moves;
27490 return(table->
keysZ);
27492 zddGroupMoveOutOfMem:
27493 while (*moves != NULL) {
27494 move = (*moves)->
next;
27520 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
27531 xsize = xbot - xtop + 1;
27533 while ((
unsigned) ybot < table->subtableZ[ybot].next)
27536 ysize = ybot - ytop + 1;
27539 for (i = 1; i <= ysize; i++) {
27540 for (j = 1; j <= xsize; j++) {
27553 for (i = 0; i < ysize - 1; i++) {
27561 for (i = 0; i < xsize - 1; i++) {
27568 if (pr > 0) (void) fprintf(table->
out,
"zddGroupMoveBackward:\n");
27597 for (move = moves; move != NULL; move = move->
next) {
27598 if (move->
size < size) {
27603 for (move = moves; move != NULL; move = move->
next) {
27604 if (move->
size == size)
return(1);
27608 if (!res)
return(0);
27610 if (pr > 0) (void) fprintf(table->
out,
"zddGroupSiftingBackward:\n");
27616 if (!res)
return(0);
27650 if (treenode != table->
treeZ) {
27651 for (i = low; i < high; i++)
27658 saveindex = treenode->
index;
27660 auxnode = treenode;
27662 auxnode->
index = newindex;
27663 if (auxnode->
parent == NULL ||
27666 auxnode = auxnode->
parent;
27804 int v, top_l, top_u;
27805 DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
27806 DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
27807 DdNode *Isub0, *Isub1, *Id;
27808 DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id;
27810 DdNode *term0, *term1, *sum;
27811 DdNode *Lv, *Uv, *Lnv, *Unv;
27826 if (U == zero || L == one) {
27827 printf(
"*** ERROR : illegal condition for ISOP (U < L).\n");
27853 v =
ddMin(top_l, top_u);
27888 if (Lsub1 == NULL) {
27895 Isub0 =
cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
27896 if (Isub0 == NULL) {
27910 Isub1 =
cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
27911 if (Isub1 == NULL) {
27931 if (Lsuper0 == NULL) {
27940 if (Lsuper1 == NULL) {
28016 if (term0 == NULL) {
28030 if (term1 == NULL) {
28073 if (zdd_Isub0 != zdd_zero) {
28087 if (zdd_Isub1 != zdd_zero) {
28142 int v, top_l, top_u;
28143 DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
28144 DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
28145 DdNode *Isub0, *Isub1, *Id;
28147 DdNode *term0, *term1, *sum;
28148 DdNode *Lv, *Uv, *Lnv, *Unv;
28165 v =
ddMin(top_l, top_u);
28200 if (Lsub1 == NULL) {
28208 if (Isub0 == NULL) {
28215 if (Isub1 == NULL) {
28226 if (Lsuper0 == NULL) {
28233 if (Lsuper1 == NULL) {
28288 if (term0 == NULL) {
28298 if (term1 == NULL) {
28371 if (node == dd->
one)
28373 if (node == dd->
zero)
28406 if (fd != dd->
zero) {
28542 #define CUDD_SWAP_MOVE 0 28543 #define CUDD_LINEAR_TRANSFORM_MOVE 1 28544 #define CUDD_INVERSE_TRANSFORM_MOVE 2 28639 size = table->
sizeZ;
28640 empty = table->
zero;
28647 goto cuddZddSiftingOutOfMem;
28649 var =
ALLOC(
int, size);
28652 goto cuddZddSiftingOutOfMem;
28655 for (i = 0; i < size; i++) {
28656 x = table->
permZ[i];
28671 x = table->
permZ[var[i]];
28672 if (x < lower || x > upper)
continue;
28674 previousSize = table->
keysZ;
28678 goto cuddZddSiftingOutOfMem;
28680 if (table->
keysZ < (
unsigned) previousSize) {
28681 (void) fprintf(table->
out,
"-");
28682 }
else if (table->
keysZ > (
unsigned) previousSize) {
28683 (void) fprintf(table->
out,
"+");
28684 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keysZ , var[i]);
28686 (void) fprintf(table->
out,
"=");
28688 fflush(table->
out);
28697 cuddZddSiftingOutOfMem:
28700 if (var != NULL)
FREE(var);
28734 int xindex, yindex;
28735 int xslots, yslots;
28736 int xshift, yshift;
28737 int oldxkeys, oldykeys;
28738 int newxkeys, newykeys;
28741 DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00;
28742 DdNode *newf1, *newf0, *g, *next, *previous;
28770 newykeys = oldykeys;
28777 g = special = NULL;
28778 for (i = 0; i < xslots; i++) {
28780 if (f == NULL)
continue;
28782 while (f != NULL) {
28788 if ((
int) f1->
index == yindex &&
cuddE(f1) == empty &&
28789 (
int) f0->
index != yindex) {
28803 for (i = 0; i < yslots; i++) {
28805 while (f != NULL) {
28815 while (f != NULL) {
28829 posn =
ddHash(f11, f0, yshift);
28830 f->
next = ylist[posn];
28840 while (f != NULL) {
28842 table->swapSteps++;
28847 if ((
int) f1->
index == yindex || (
int) f1->
index == xindex) {
28850 f11 =
empty; f10 = f1;
28853 if ((
int) f0->
index == yindex || (
int) f0->
index == xindex) {
28856 f01 =
empty; f00 = f0;
28859 if (f01 == empty) {
28864 posn =
ddHash(f01, f10, yshift);
28866 newf1 = ylist[posn];
28868 while (newf1 != NULL) {
28869 if (
cuddT(newf1) == f01 &&
cuddE(newf1) == f10 &&
28870 (
int) newf1->
index == yindex) {
28874 newf1 = newf1->
next;
28876 if (newf1 == NULL) {
28879 goto zddSwapOutOfMem;
28880 newf1->
index = yindex; newf1->
ref = 1;
28881 cuddT(newf1) = f01;
28882 cuddE(newf1) = f10;
28887 newf1->
next = ylist[posn];
28888 ylist[posn] = newf1;
28897 if (f11 == empty) {
28902 posn =
ddHash(f11, f00, yshift);
28904 newf0 = ylist[posn];
28905 while (newf0 != NULL) {
28906 if (
cuddT(newf0) == f11 &&
cuddE(newf0) == f00 &&
28907 (
int) newf0->
index == yindex) {
28911 newf0 = newf0->
next;
28913 if (newf0 == NULL) {
28916 goto zddSwapOutOfMem;
28917 newf0->
index = yindex; newf0->
ref = 1;
28923 newf0->
next = ylist[posn];
28924 ylist[posn] = newf0;
28935 posn =
ddHash(newf1, newf0, xshift);
28937 f->
next = xlist[posn];
28945 for (i = 0; i < yslots; i++) {
28948 while (f != NULL) {
28955 if (previous == NULL)
28958 previous->
next = next;
28959 }
else if ((
int) f->
index == xindex) {
28960 if (previous == NULL)
28963 previous->
next = next;
28967 posn =
ddHash(f1, empty, yshift);
28969 newf1 = ylist[posn];
28970 while (newf1 != NULL) {
28971 if (
cuddT(newf1) == f1 &&
cuddE(newf1) == empty &&
28972 (
int) newf1->
index == yindex) {
28976 newf1 = newf1->
next;
28978 if (newf1 == NULL) {
28981 goto zddSwapOutOfMem;
28982 newf1->
index = yindex; newf1->
ref = 1;
28988 newf1->
next = ylist[posn];
28989 ylist[posn] = newf1;
28990 if (posn == i && previous == NULL)
28998 posn =
ddHash(newf1, f0, xshift);
29001 f->
next = xlist[posn];
29014 table->
keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
29020 (void) fprintf(table->
out,
"x = %d y = %d\n", x, y);
29025 return (table->
keysZ);
29028 (void) fprintf(table->
err,
"Error: cuddZddSwapInPlace out of memory\n");
29063 initial_size = table->
keysZ;
29076 goto cuddZddLinearAuxOutOfMem;
29080 goto cuddZddLinearAuxOutOfMem;
29082 }
else if (x == xHigh) {
29086 goto cuddZddLinearAuxOutOfMem;
29090 goto cuddZddLinearAuxOutOfMem;
29092 }
else if ((x - xLow) > (xHigh - x)) {
29096 goto cuddZddLinearAuxOutOfMem;
29099 assert(moveUp == NULL || moveUp->
x == x);
29102 if (moveUp == (
Move *) CUDD_OUT_OF_MEM)
29103 goto cuddZddLinearAuxOutOfMem;
29107 goto cuddZddLinearAuxOutOfMem;
29113 goto cuddZddLinearAuxOutOfMem;
29117 assert(moveDown == NULL || moveDown->
y == x);
29120 if (moveDown == (
Move *) CUDD_OUT_OF_MEM)
29121 goto cuddZddLinearAuxOutOfMem;
29125 goto cuddZddLinearAuxOutOfMem;
29128 while (moveDown != NULL) {
29129 move = moveDown->
next;
29133 while (moveUp != NULL) {
29134 move = moveUp->
next;
29141 cuddZddLinearAuxOutOfMem:
29143 while (moveDown != NULL) {
29144 move = moveDown->
next;
29149 if (moveUp != (
Move *) CUDD_OUT_OF_MEM) {
29150 while (moveUp != NULL) {
29151 move = moveUp->
next;
29190 limitSize = table->
keysZ;
29193 while (x >= xLow) {
29196 goto cuddZddLinearUpOutOfMem;
29199 goto cuddZddLinearUpOutOfMem;
29202 goto cuddZddLinearUpOutOfMem;
29205 move->
next = moves;
29208 if (newsize > size) {
29214 if (newsize == 0)
goto cuddZddLinearUpOutOfMem;
29216 if (newsize != size) {
29217 (void) fprintf(table->
err,
"Change in size after identity transformation! From %d to %d\n",size,newsize);
29226 if ((
double)size > (double)limitSize * table->
maxGrowth)
29228 if (size < limitSize)
29236 cuddZddLinearUpOutOfMem:
29237 while (moves != NULL) {
29238 move = moves->
next;
29275 limitSize = table->
keysZ;
29278 while (y <= xHigh) {
29281 goto cuddZddLinearDownOutOfMem;
29284 goto cuddZddLinearDownOutOfMem;
29287 goto cuddZddLinearDownOutOfMem;
29290 move->
next = moves;
29293 if (newsize > size) {
29299 if (newsize == 0)
goto cuddZddLinearDownOutOfMem;
29300 if (newsize != size) {
29301 (void) fprintf(table->
err,
"Change in size after identity transformation! From %d to %d\n",size,newsize);
29309 if ((
double)size > (double)limitSize * table->
maxGrowth)
29311 if (size < limitSize)
29319 cuddZddLinearDownOutOfMem:
29320 while (moves != NULL) {
29321 move = moves->
next;
29355 for (move = moves; move != NULL; move = move->
next) {
29356 if (move->
size < size) {
29361 for (move = moves; move != NULL; move = move->
next) {
29362 if (move->
size == size)
return(1);
29365 if (!res)
return(0);
29372 if (!res)
return(0);
29398 Move *invmoves = NULL;
29403 for (move = moves; move != NULL; move = move->
next) {
29405 if (invmove == NULL)
goto cuddZddUndoMovesOutOfMem;
29406 invmove->
x = move->
x;
29407 invmove->
y = move->
y;
29408 invmove->
next = invmoves;
29409 invmoves = invmove;
29413 if (!size)
goto cuddZddUndoMovesOutOfMem;
29417 if (!size)
goto cuddZddUndoMovesOutOfMem;
29419 if (!size)
goto cuddZddUndoMovesOutOfMem;
29422 (void) fprintf(table->
err,
"Unforseen event in ddUndoMoves!\n");
29426 if (!size)
goto cuddZddUndoMovesOutOfMem;
29428 if (!size)
goto cuddZddUndoMovesOutOfMem;
29430 invmove->
size = size;
29435 cuddZddUndoMovesOutOfMem:
29436 while (invmoves != NULL) {
29437 move = invmoves->
next;
29525 #define DD_MAX_SUBTABLE_SPARSITY 8 29615 unsigned int nextDyn;
29617 unsigned int initialSize;
29618 unsigned int finalSize;
29620 unsigned long localTime;
29623 if (table->
keysZ - table->
deadZ < (
unsigned) minsize)
29637 empty = table->
zero;
29643 while (hook != NULL) {
29644 int res = (hook->
f)(table,
"ZDD", (
void *)heuristic);
29645 if (res == 0)
return(0);
29654 initialSize = table->
keysZ;
29656 switch(heuristic) {
29659 (void) fprintf(table->
out,
"#:I_RANDOM ");
29665 (void) fprintf(table->
out,
"#:I_SIFTING ");
29669 (void) fprintf(table->
out,
"#:I_LINSIFT ");
29672 (void) fprintf(table->
err,
"Unsupported ZDD reordering method\n");
29675 (void) fprintf(table->
out,
"%8d: initial size",initialSize);
29681 (void) fprintf(table->
out,
"\n");
29682 finalSize = table->
keysZ;
29683 (void) fprintf(table->
out,
"#:F_REORDER %8d: final size\n",finalSize);
29684 (void) fprintf(table->
out,
"#:T_REORDER %8g: total time (sec)\n",
29686 (void) fprintf(table->
out,
"#:N_REORDER %8d: total swaps\n",
29711 while (hook != NULL) {
29712 int res = (hook->
f)(table,
"ZDD", (
void *)localTime);
29713 if (res == 0)
return(0);
29762 if (table->
sizeZ == 0)
29765 empty = table->
zero;
29774 if (invpermZ == NULL) {
29778 for (i = 0; i < table->
size; i++) {
29779 int index = table->
invperm[i];
29780 int indexZ = index * M;
29781 int levelZ = table->
permZ[indexZ];
29782 levelZ = (levelZ / M) * M;
29783 for (j = 0; j < M; j++) {
29784 invpermZ[M * i + j] = table->
invpermZ[levelZ + j];
29891 int xindex, yindex;
29892 int xslots, yslots;
29893 int xshift, yshift;
29894 int oldxkeys, oldykeys;
29895 int newxkeys, newykeys;
29898 DdNode *f, *f1, *f0, *f11, *f10, *f01, *f00;
29899 DdNode *newf1, *newf0, *next;
29926 newykeys = oldykeys;
29936 for (i = 0; i < xslots; i++) {
29937 previousP = &(xlist[i]);
29939 while (f != NULL) {
29946 previousP = &(f->
next);
29950 lastP = &(f->
next);
29960 table->swapSteps += oldxkeys - newxkeys;
29967 while (f != NULL) {
29971 if ((
int) f1->
index == yindex) {
29974 f11 =
empty; f10 = f1;
29977 if ((
int) f0->
index == yindex) {
29980 f01 =
empty; f00 = f0;
29986 if (f11 == empty) {
29987 if (f01 != empty) {
29996 posn =
ddHash(f11, f01, xshift);
29998 newf1 = xlist[posn];
29999 while (newf1 != NULL) {
30000 if (
cuddT(newf1) == f11 &&
cuddE(newf1) == f01) {
30004 newf1 = newf1->
next;
30006 if (newf1 == NULL) {
30009 goto zddSwapOutOfMem;
30010 newf1->
index = xindex; newf1->
ref = 1;
30011 cuddT(newf1) = f11;
30012 cuddE(newf1) = f01;
30017 newf1->
next = xlist[posn];
30018 xlist[posn] = newf1;
30029 if (f10 == empty) {
30034 posn =
ddHash(f10, f00, xshift);
30036 newf0 = xlist[posn];
30037 while (newf0 != NULL) {
30038 if (
cuddT(newf0) == f10 &&
cuddE(newf0) == f00) {
30042 newf0 = newf0->
next;
30044 if (newf0 == NULL) {
30047 goto zddSwapOutOfMem;
30048 newf0->
index = xindex; newf0->
ref = 1;
30054 newf0->
next = xlist[posn];
30055 xlist[posn] = newf0;
30066 posn =
ddHash(newf1, newf0, yshift);
30068 f->
next = ylist[posn];
30076 for (i = 0; i < yslots; i++) {
30077 previousP = &(ylist[i]);
30079 while (f != NULL) {
30088 previousP = &(f->
next);
30108 table->
permZ[xindex] = y; table->
permZ[yindex] = x;
30111 table->
keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
30116 return (table->
keysZ);
30119 (void) fprintf(table->
err,
"Error: cuddZddSwapInPlace out of memory\n");
30159 Move *moves, *move;
30166 assert(lower >= 0 && upper < table->sizeZ && lower <= upper);
30169 nvars = upper - lower + 1;
30172 for (i = 0; i < iterate; i++) {
30175 for (max = -1, j = lower; j <= upper; j++) {
30182 modulo = upper - pivot;
30190 modulo = pivot - lower - 1;
30207 previousSize = table->
keysZ;
30210 goto cuddZddSwappingOutOfMem;
30214 goto cuddZddSwappingOutOfMem;
30216 while (moves != NULL) {
30217 move = moves->
next;
30222 if (table->
keysZ < (
unsigned) previousSize) {
30223 (void) fprintf(table->
out,
"-");
30224 }
else if (table->
keysZ > (
unsigned) previousSize) {
30225 (void) fprintf(table->
out,
"+");
30227 (void) fprintf(table->
out,
"=");
30229 fflush(table->
out);
30235 cuddZddSwappingOutOfMem:
30236 while (moves != NULL) {
30237 move = moves->
next;
30282 size = table->
sizeZ;
30289 goto cuddZddSiftingOutOfMem;
30291 var =
ALLOC(
int, size);
30294 goto cuddZddSiftingOutOfMem;
30297 for (i = 0; i < size; i++) {
30298 x = table->
permZ[i];
30313 x = table->
permZ[var[i]];
30314 if (x < lower || x > upper)
continue;
30316 previousSize = table->
keysZ;
30320 goto cuddZddSiftingOutOfMem;
30322 if (table->
keysZ < (
unsigned) previousSize) {
30323 (void) fprintf(table->
out,
"-");
30324 }
else if (table->
keysZ > (
unsigned) previousSize) {
30325 (void) fprintf(table->
out,
"+");
30326 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keysZ , var[i]);
30328 (void) fprintf(table->
out,
"=");
30330 fflush(table->
out);
30339 cuddZddSiftingOutOfMem:
30342 if (var != NULL)
FREE(var);
30371 Move *move, *moves;
30374 int x_next, y_next;
30378 tmp = x; x = y; y = tmp;
30381 x_ref = x; y_ref = y;
30386 limit_size = table->
keysZ;
30389 if (x_next == y_next) {
30392 goto zddSwapAnyOutOfMem;
30395 goto zddSwapAnyOutOfMem;
30399 move->
next = moves;
30404 goto zddSwapAnyOutOfMem;
30407 goto zddSwapAnyOutOfMem;
30411 move->
next = moves;
30416 goto zddSwapAnyOutOfMem;
30419 goto zddSwapAnyOutOfMem;
30423 move->
next = moves;
30426 tmp = x; x = y; y = tmp;
30428 }
else if (x == y_next) {
30431 goto zddSwapAnyOutOfMem;
30434 goto zddSwapAnyOutOfMem;
30438 move->
next = moves;
30441 tmp = x; x = y; y = tmp;
30445 goto zddSwapAnyOutOfMem;
30448 goto zddSwapAnyOutOfMem;
30452 move->
next = moves;
30457 goto zddSwapAnyOutOfMem;
30460 goto zddSwapAnyOutOfMem;
30464 move->
next = moves;
30467 x = x_next; y = y_next;
30472 if (x_next > y_ref)
30475 if ((
double) size > table->
maxGrowth * (
double) limit_size)
30477 if (size < limit_size)
30480 if (y_next >= x_ref) {
30483 goto zddSwapAnyOutOfMem;
30486 goto zddSwapAnyOutOfMem;
30490 move->
next = moves;
30496 zddSwapAnyOutOfMem:
30497 while (moves != NULL) {
30498 move = moves->
next;
30535 initial_size = table->
keysZ;
30547 if (moveDown == NULL)
30548 goto cuddZddSiftingAuxOutOfMem;
30553 goto cuddZddSiftingAuxOutOfMem;
30556 else if (x == x_high) {
30559 if (moveUp == NULL)
30560 goto cuddZddSiftingAuxOutOfMem;
30564 goto cuddZddSiftingAuxOutOfMem;
30566 else if ((x - x_low) > (x_high - x)) {
30570 if (moveDown == NULL)
30571 goto cuddZddSiftingAuxOutOfMem;
30574 if (moveUp == NULL)
30575 goto cuddZddSiftingAuxOutOfMem;
30579 goto cuddZddSiftingAuxOutOfMem;
30584 if (moveUp == NULL)
30585 goto cuddZddSiftingAuxOutOfMem;
30589 if (moveDown == NULL)
30590 goto cuddZddSiftingAuxOutOfMem;
30595 goto cuddZddSiftingAuxOutOfMem;
30598 while (moveDown != NULL) {
30599 move = moveDown->
next;
30603 while (moveUp != NULL) {
30604 move = moveUp->
next;
30611 cuddZddSiftingAuxOutOfMem:
30612 while (moveDown != NULL) {
30613 move = moveDown->
next;
30617 while (moveUp != NULL) {
30618 move = moveUp->
next;
30652 int limit_size = initial_size;
30656 while (y >= x_low) {
30659 goto cuddZddSiftingUpOutOfMem;
30662 goto cuddZddSiftingUpOutOfMem;
30666 move->
next = moves;
30669 if ((
double)size > (double)limit_size * table->
maxGrowth)
30671 if (size < limit_size)
30679 cuddZddSiftingUpOutOfMem:
30680 while (moves != NULL) {
30681 move = moves->
next;
30715 int limit_size = initial_size;
30719 while (y <= x_high) {
30722 goto cuddZddSiftingDownOutOfMem;
30725 goto cuddZddSiftingDownOutOfMem;
30729 move->
next = moves;
30732 if ((
double)size > (double)limit_size * table->
maxGrowth)
30734 if (size < limit_size)
30742 cuddZddSiftingDownOutOfMem:
30743 while (moves != NULL) {
30744 move = moves->
next;
30781 for (move = moves, i = 0; move != NULL; move = move->
next, i++) {
30782 if (move->
size < size) {
30788 for (move = moves, i = 0; move != NULL; move = move->
next, i++) {
30794 if (i_best == -1 && res == size)
30850 unsigned int slots, oldslots;
30855 (void) fflush(table->
out);
30867 for (i = 0; i < table->
sizeZ; i++) {
30871 oldslots <= table->initSlots)
continue;
30873 slots = oldslots >> 1;
30877 MMoutOfMemory = saveHandler;
30878 if (nodelist == NULL) {
30886 (void) fprintf(table->
err,
30887 "shrunk layer %d (%d keys) from %d to %d slots\n",
30891 for (j = 0; (unsigned) j < slots; j++) {
30892 nodelist[j] = NULL;
30895 for (j = 0; (unsigned) j < oldslots; j++) {
30896 node = oldnodelist[j];
30897 while (node != NULL) {
30900 node->
next = nodelist[posn];
30901 nodelist[posn] = node;
30908 table->
slots += slots - oldslots;
30949 unsigned long localTime;
30958 initialSize = table->
keysZ;
30959 (void) fprintf(table->
out,
"#:I_SHUFFLE %8d: initial size\n",
30963 numvars = table->
sizeZ;
30965 for (level = 0; level <
numvars; level++) {
30966 index = permutation[level];
30967 position = table->
permZ[index];
30969 previousSize = table->
keysZ;
30971 result =
zddSiftUp(table,position,level);
30972 if (!result)
return(0);
30974 if (table->
keysZ < (
unsigned) previousSize) {
30975 (void) fprintf(table->
out,
"-");
30976 }
else if (table->
keysZ > (
unsigned) previousSize) {
30977 (void) fprintf(table->
out,
"+");
30979 (void) fprintf(table->
out,
"=");
30981 fflush(table->
out);
30986 (void) fprintf(table->
out,
"\n");
30987 finalSize = table->
keysZ;
30988 (void) fprintf(table->
out,
"#:F_SHUFFLE %8d: final size\n",finalSize);
30989 (void) fprintf(table->
out,
"#:T_SHUFFLE %8g: total time (sec)\n",
30991 (void) fprintf(table->
out,
"#:N_SHUFFLE %8d: total swaps\n",
31023 while (y >= xLow) {
31054 if (treenode == NULL)
return;
31057 if (treenode->
child != NULL) {
31060 if (treenode->
younger != NULL)
31242 if (p_top < q_top) {
31244 }
else if (p_top > q_top) {
31285 DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
31286 unsigned int topf,topg,toph,v,top;
31292 if (f == (empty =
DD_ZERO(dd))) {
31298 v =
ddMin(topg,toph);
31299 top =
ddMin(topf,v);
31302 if (f == tautology) {
31314 if (g == tautology) {
31315 if (h == empty)
return(f);
31327 v =
ddMin(topg,toph);
31331 if (r == NULL)
return(NULL);
31332 }
else if (topf > v) {
31341 Hv =
empty; Hvn = h;
31346 if (e == NULL)
return(NULL);
31357 Gv =
empty; Gvn = g;
31362 Hv =
empty; Hvn = h;
31367 if (e == NULL)
return(NULL);
31434 if (p_top < q_top) {
31436 if (e == NULL)
return (NULL);
31444 }
else if (p_top > q_top) {
31446 if (e == NULL)
return(NULL);
31456 if (t == NULL)
return(NULL);
31523 if (p_top < q_top) {
31525 if (res == NULL)
return(NULL);
31526 }
else if (p_top > q_top) {
31528 if (res == NULL)
return(NULL);
31531 if (t == NULL)
return(NULL);
31598 if (p_top < q_top) {
31600 if (e == NULL)
return(NULL);
31608 }
else if (p_top > q_top) {
31610 if (res == NULL)
return(NULL);
31613 if (t == NULL)
return(NULL);
31655 int top_var, level;
31674 if (top_var > level) {
31676 if (res == NULL)
return(NULL);
31677 }
else if (top_var == level) {
31679 if (res == NULL)
return(NULL);
31682 if (t == NULL)
return(NULL);
31737 if (zvar == NULL) {
31786 if (zvar == NULL) {
31827 int top_var, level;
31848 if (top_var > level) {
31850 }
else if (top_var == level) {
31854 if (t == NULL)
return(NULL);
31896 int top_var, level;
31915 if (top_var > level) {
31918 else if (top_var == level) {
31923 if (t == NULL)
return(NULL);
32055 #define ZDD_MV_OOM (Move *)1 32133 DdNode *f, *f0, *f1, *f01, *f00, *f11, *f10;
32138 int TotalRefCount = 0;
32141 empty = table->
zero;
32146 while (f != NULL) {
32150 if ((
int) f1->
index == yindex) {
32156 if ((
int) f0->
index != yindex) {
32162 if ((
int) f0->
index == yindex) {
32175 if ((xsymmy == 0) && (xsymmyp == 0))
32188 if (
cuddE(f) != empty)
32189 TotalRefCount += f->
ref;
32194 symm_found = (arccount == TotalRefCount);
32195 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 32198 (void) fprintf(table->
out,
32199 "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
32200 xindex,yindex,x,y);
32204 return(symm_found);
32249 nvars = table->
sizeZ;
32256 goto cuddZddSymmSiftingOutOfMem;
32258 var =
ALLOC(
int, nvars);
32261 goto cuddZddSymmSiftingOutOfMem;
32264 for (i = 0; i < nvars; i++) {
32265 x = table->
permZ[i];
32273 for (i = lower; i <= upper; i++)
32277 for (i = 0; i < iteration; i++) {
32284 x = table->
permZ[var[i]];
32286 previousSize = table->
keysZ;
32288 if (x < lower || x > upper)
continue;
32292 goto cuddZddSymmSiftingOutOfMem;
32294 if (table->
keysZ < (
unsigned) previousSize) {
32295 (void) fprintf(table->
out,
"-");
32296 }
else if (table->
keysZ > (
unsigned) previousSize) {
32297 (void) fprintf(table->
out,
"+");
32299 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keysZ, var[i]);
32302 (void) fprintf(table->
out,
"=");
32304 fflush(table->
out);
32315 (void) fprintf(table->
out,
"\n#:S_SIFTING %8d: symmetric variables\n",symvars);
32316 (void) fprintf(table->
out,
"#:G_SIFTING %8d: symmetric groups\n",symgroups);
32321 cuddZddSymmSiftingOutOfMem:
32376 initialSize = table->
keysZ;
32378 nvars = table->
sizeZ;
32385 goto cuddZddSymmSiftingConvOutOfMem;
32387 var =
ALLOC(
int, nvars);
32390 goto cuddZddSymmSiftingConvOutOfMem;
32393 for (i = 0; i < nvars; i++) {
32394 x = table->
permZ[i];
32404 for (i = lower; i <= upper; i++)
32408 for (i = 0; i < iteration; i++) {
32415 x = table->
permZ[var[i]];
32416 if (x < lower || x > upper)
continue;
32420 previousSize = table->
keysZ;
32424 goto cuddZddSymmSiftingConvOutOfMem;
32426 if (table->
keysZ < (
unsigned) previousSize) {
32427 (void) fprintf(table->
out,
"-");
32428 }
else if (table->
keysZ > (
unsigned) previousSize) {
32429 (void) fprintf(table->
out,
"+");
32431 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keysZ, var[i]);
32434 (void) fprintf(table->
out,
"=");
32436 fflush(table->
out);
32442 while ((
unsigned) initialSize > table->
keysZ) {
32443 initialSize = table->
keysZ;
32445 (void) fprintf(table->
out,
"\n");
32448 for (x = lower, classes = 0; x <= upper; x++, classes++) {
32460 qsort((
void *)var,classes,
sizeof(
int),(
DD_QSFP)cuddZddUniqueCompare);
32464 for (i = 0; i < iteration; i++) {
32471 x = table->
permZ[var[i]];
32474 previousSize = table->
keysZ;
32478 goto cuddZddSymmSiftingConvOutOfMem;
32480 if (table->
keysZ < (
unsigned) previousSize) {
32481 (void) fprintf(table->
out,
"-");
32482 }
else if (table->
keysZ > (
unsigned) previousSize) {
32483 (void) fprintf(table->
out,
"+");
32485 (void) fprintf(table->
out,
"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->
keysZ, var[i]);
32488 (void) fprintf(table->
out,
"=");
32490 fflush(table->
out);
32499 (void) fprintf(table->
out,
"\n#:S_SIFTING %8d: symmetric variables\n",
32501 (void) fprintf(table->
out,
"#:G_SIFTING %8d: symmetric groups\n",
32510 cuddZddSymmSiftingConvOutOfMem:
32556 int init_group_size, final_group_size;
32558 initial_size = table->
keysZ;
32564 for (i = x; i > x_low; i--) {
32576 for (i = x; i < x_high; i++) {
32581 while ((
unsigned) topbot < table->subtableZ[topbot].next)
32593 while ((
unsigned) x < table->subtableZ[x].next)
32597 init_group_size = x - i + 1;
32603 goto cuddZddSymmSiftingAuxOutOfMem;
32605 if (move_down == NULL ||
32609 if (move_down != NULL)
32614 while ((
unsigned) i < table->subtableZ[i].next) {
32617 final_group_size = i - x + 1;
32619 if (init_group_size == final_group_size) {
32623 move_down, initial_size);
32626 initial_size = table->
keysZ;
32639 goto cuddZddSymmSiftingAuxOutOfMem;
32641 else if (x == x_high) {
32643 while ((
unsigned) x < table->subtableZ[x].next)
32648 while ((
unsigned) i < table->subtableZ[i].next) {
32651 init_group_size = i - x + 1;
32656 goto cuddZddSymmSiftingAuxOutOfMem;
32658 if (move_up == NULL ||
32662 if (move_up != NULL)
32665 while ((
unsigned) x < table->subtableZ[x].next)
32669 final_group_size = x - i + 1;
32671 if (init_group_size == final_group_size) {
32678 initial_size = table->
keysZ;
32691 goto cuddZddSymmSiftingAuxOutOfMem;
32693 else if ((x - x_low) > (x_high - x)) {
32696 while ((
unsigned) x < table->subtableZ[x].next)
32703 goto cuddZddSymmSiftingAuxOutOfMem;
32705 if (move_down != NULL) {
32712 while ((
unsigned) i < table->subtableZ[i].next) {
32715 init_group_size = i - x + 1;
32719 goto cuddZddSymmSiftingAuxOutOfMem;
32721 if (move_up == NULL ||
32725 if (move_up != NULL) {
32729 while ((
unsigned) x < table->subtableZ[x].next)
32733 final_group_size = x - i + 1;
32735 if (init_group_size == final_group_size) {
32742 while (move_down != NULL) {
32743 move = move_down->
next;
32747 initial_size = table->
keysZ;
32760 goto cuddZddSymmSiftingAuxOutOfMem;
32764 while ((
unsigned) x < table->subtableZ[x].next)
32771 goto cuddZddSymmSiftingAuxOutOfMem;
32773 if (move_up != NULL) {
32777 while ((
unsigned) x < table->subtableZ[x].next)
32781 init_group_size = x - i + 1;
32786 goto cuddZddSymmSiftingAuxOutOfMem;
32788 if (move_down == NULL ||
32792 if (move_down != NULL) {
32799 while ((
unsigned) i < table->subtableZ[i].next) {
32802 final_group_size = i - x + 1;
32804 if (init_group_size == final_group_size) {
32811 while (move_up != NULL) {
32812 move = move_up->
next;
32816 initial_size = table->
keysZ;
32829 goto cuddZddSymmSiftingAuxOutOfMem;
32832 while (move_down != NULL) {
32833 move = move_down->
next;
32837 while (move_up != NULL) {
32838 move = move_up->
next;
32845 cuddZddSymmSiftingAuxOutOfMem:
32847 while (move_down != NULL) {
32848 move = move_down->
next;
32854 while (move_up != NULL) {
32855 move = move_up->
next;
32895 int init_group_size, final_group_size;
32897 initial_size = table->
keysZ;
32904 init_group_size = x - i + 1;
32910 goto cuddZddSymmSiftingConvAuxOutOfMem;
32912 if (move_down == NULL ||
32916 if (move_down != NULL)
32919 while ((
unsigned) x < table->subtableZ[x].next)
32924 while ((
unsigned) i < table->subtableZ[i].next) {
32927 final_group_size = i - x + 1;
32929 if (init_group_size == final_group_size) {
32936 initial_size = table->
keysZ;
32949 goto cuddZddSymmSiftingConvAuxOutOfMem;
32951 else if (x == x_high) {
32953 while ((
unsigned) x < table->subtableZ[x].next)
32958 while ((
unsigned) i < table->subtableZ[i].next) {
32961 init_group_size = i - x + 1;
32966 goto cuddZddSymmSiftingConvAuxOutOfMem;
32968 if (move_up == NULL ||
32972 if (move_up != NULL)
32975 while ((
unsigned) x < table->subtableZ[x].next)
32979 final_group_size = x - i + 1;
32981 if (init_group_size == final_group_size) {
32988 initial_size = table->
keysZ;
33001 goto cuddZddSymmSiftingConvAuxOutOfMem;
33003 else if ((x - x_low) > (x_high - x)) {
33009 goto cuddZddSymmSiftingConvAuxOutOfMem;
33011 if (move_down != NULL) {
33015 while ((
unsigned) x < table->subtableZ[x].next)
33020 while ((
unsigned) i < table->subtableZ[i].next) {
33023 init_group_size = i - x + 1;
33027 goto cuddZddSymmSiftingConvAuxOutOfMem;
33029 if (move_up == NULL ||
33033 if (move_up != NULL) {
33037 while ((
unsigned) x < table->subtableZ[x].next)
33041 final_group_size = x - i + 1;
33043 if (init_group_size == final_group_size) {
33050 while (move_down != NULL) {
33051 move = move_down->
next;
33055 initial_size = table->
keysZ;
33068 goto cuddZddSymmSiftingConvAuxOutOfMem;
33077 goto cuddZddSymmSiftingConvAuxOutOfMem;
33079 if (move_up != NULL) {
33083 while ((
unsigned) x < table->subtableZ[x].next)
33087 init_group_size = x - i + 1;
33092 goto cuddZddSymmSiftingConvAuxOutOfMem;
33094 if (move_down == NULL ||
33098 if (move_down != NULL) {
33102 while ((
unsigned) x < table->subtableZ[x].next)
33107 while ((
unsigned) i < table->subtableZ[i].next) {
33110 final_group_size = i - x + 1;
33112 if (init_group_size == final_group_size) {
33119 while (move_up != NULL) {
33120 move = move_up->
next;
33124 initial_size = table->
keysZ;
33137 goto cuddZddSymmSiftingConvAuxOutOfMem;
33140 while (move_down != NULL) {
33141 move = move_down->
next;
33145 while (move_up != NULL) {
33146 move = move_up->
next;
33153 cuddZddSymmSiftingConvAuxOutOfMem:
33155 while (move_down != NULL) {
33156 move = move_down->
next;
33162 while (move_up != NULL) {
33163 move = move_up->
next;
33202 int limit_size = initial_size;
33207 while (y >= x_low) {
33222 goto cuddZddSymmSifting_upOutOfMem;
33225 goto cuddZddSymmSifting_upOutOfMem;
33229 move->
next = moves;
33234 if (size < limit_size)
33242 if (size < limit_size)
33251 cuddZddSymmSifting_upOutOfMem:
33252 while (moves != NULL) {
33253 move = moves->
next;
33290 int limit_size = initial_size;
33291 int i, gxtop, gybot;
33295 while (y <= x_high) {
33313 goto cuddZddSymmSifting_downOutOfMem;
33316 goto cuddZddSymmSifting_downOutOfMem;
33320 move->
next = moves;
33325 if (size < limit_size)
33335 if (size < limit_size)
33344 cuddZddSymmSifting_downOutOfMem:
33345 while (moves != NULL) {
33346 move = moves->
next;
33382 for (move = moves, i = 0; move != NULL; move = move->
next, i++) {
33383 if (move->
size < size) {
33389 for (move = moves, i = 0; move != NULL; move = move->
next, i++) {
33390 if (i == i_best)
break;
33394 if (!res)
return(0);
33399 if (i_best == -1 && res == size)
33431 int i, temp, gxtop, gxbot, gybot, yprev;
33446 while (y > gxtop) {
33475 goto zdd_group_moveOutOfMem;
33496 goto zdd_group_moveOutOfMem;
33500 move->
next = *moves;
33503 return(table->
keysZ);
33505 zdd_group_moveOutOfMem:
33506 while (*moves != NULL) {
33507 move = (*moves)->
next;
33536 int i, temp, gxtop, gxbot, gybot, yprev;
33550 while (y > gxtop) {
33622 int TotalSymmGroups = 0;
33624 for (i = lower; i <= upper; i++) {
33639 *symvars = TotalSymm;
33640 *symgroups = TotalSymmGroups;
int cuddZddNextHigh(DdManager *table, int x)
static int ddSiftUp2(DdManager *table, int x, int xLow)
static void zddMergeGroups(DdManager *table, MtrNode *treenode, int low, int high)
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
static int getMaxBinomial(int n)
static void cuddXorLinear(DdManager *table, int x, int y)
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
static Move * cuddZddSymmSifting_up(DdManager *table, int x, int x_low, int initial_size)
static int make_random(DdManager *table, int lower)
DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
int Cudd_EquivDC(DdManager *dd, DdNode *F, DdNode *G, DdNode *D)
static void ddPrintMintermAux(DdManager *dd, DdNode *node, int *list)
Cudd_AggregationType groupcheck
DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
int cuddBddAlignToZdd(DdManager *table)
static void copyOrder(DdManager *table, int *array, int lower, int upper)
static int siftBackwardProb(DdManager *table, Move *moves, int size, double temp)
int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method)
unsigned short DdHalfWord
static Move * ddUndoMoves(DdManager *table, Move *moves)
static void zddFixTree(DdManager *table, MtrNode *treenode)
void EpdMultiply(EpDouble *epd1, double value)
DdGen * Cudd_FirstNode(DdManager *dd, DdNode *f, DdNode **node)
DdNode * cuddAllocNode(DdManager *unique)
#define DD_MAX_HASHTABLE_DENSITY
static int ddReorderChildren(DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
static int ddShuffle(DdManager *table, DdHalfWord *permutation, int lower, int upper)
static int ddUniqueCompareGroup(int *ptrX, int *ptrY)
static Move * cuddZddUndoMoves(DdManager *table, Move *moves)
void EpdFree(EpDouble *epd)
int st_lookup(st_table *, void *, void *)
static int zddGroupSiftingDown(DdManager *table, int x, int xHigh, Move **moves)
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
void cuddUpdateInteractionMatrix(DdManager *table, int xindex, int yindex)
static double ddCountPathsToNonZero(DdNode *N, st_table *table)
#define cuddDeallocMove(unique, node)
DdNode * Cudd_addIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
static int ddLeavesInt(DdNode *n)
Cudd_ReorderingType autoMethod
static Move * ddJumpingDown(DdManager *table, int x, int x_high, int initial_size)
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
#define cuddIZ(dd, index)
static int ddGroupSifting(DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag)
static DdHalfWord ** getMatrix(int rows, int cols)
unsigned int peakLiveNodes
static void bddVarToConst(DdNode *f, DdNode **gp, DdNode **hp, DdNode *one)
static void ddMergeGroups(DdManager *table, MtrNode *treenode, int low, int high)
static int ddDagInt(DdNode *n)
static int zddGroupSiftingBackward(DdManager *table, Move *moves, int size)
int st_lookup_int(st_table *, void *, int *)
DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
static DD_INLINE DdHashItem * cuddHashTableAlloc(DdHashTable *hash)
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
#define DD_MAX_CACHE_FRACTION
static int ddLinearAndSiftingAux(DdManager *table, int x, int xLow, int xHigh)
DdNode * Cudd_addCmpl(DdManager *dd, DdNode *f)
static int ddExchange(DdManager *table, int x, int y, double temp)
DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
#define ddLCHash3(f, g, h, shift)
void st_free_gen(st_generator *)
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
#define CUDD_GEN_ZDD_PATHS
int st_foreach(st_table *, ST_PFSR, char *)
int(* DD_QSFP)(const void *, const void *)
void cuddShrinkDeathRow(DdManager *table)
static DD_INLINE void ddFixLimits(DdManager *unique)
DdHook * preReorderingHook
static double ddCountMintermAux(DdNode *node, double max, DdHashTable *table)
static Move * cuddZddSiftingUp(DdManager *table, int x, int x_low, int initial_size)
static enum st_retval freePathPair(char *key, char *value, char *arg)
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
int cuddCollectNodes(DdNode *f, st_table *visited)
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
void cuddHashTableGenericQuit(DdHashTable *hash)
int cuddInitInteract(DdManager *table)
static Move * ddSiftingDown(DdManager *table, int x, int xHigh)
static int ddSymmGroupMove(DdManager *table, int x, int y, Move **moves)
#define DD_BDD_ITE_CONSTANT_TAG
int Cudd_BddToCubeArray(DdManager *dd, DdNode *cube, int *array)
static Move * cuddZddSiftingDown(DdManager *table, int x, int x_high, int initial_size)
static unsigned int originalSize
static void pushDown(DdHalfWord *order, int j, int level)
#define DD_STASH_FRACTION
DdNode * Cudd_ReadLogicZero(DdManager *dd)
static char rcsid [] DD_UNUSED
#define DD_ADD_ITE_CONSTANT_TAG
void st_free_table(st_table *)
struct DdManager DdManager
#define Cudd_IsConstant(node)
unsigned int maxCacheHard
static int zddSiftUp(DdManager *table, int x, int xLow)
int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method)
struct DdGen::@1::@5 nodes
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
static int bddVarToCanonicalSimple(DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp)
#define Cudd_Regular(node)
static int zdd_group_move(DdManager *table, int x, int y, Move **moves)
#define DD_MAX_LOOSE_FRACTION
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
static int bddVarToCanonical(DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp)
DdNode * cuddDynamicAllocNode(DdManager *table)
static void ddSuppInteract(DdNode *f, char *support)
static int ddWindow2(DdManager *table, int low, int high)
static int ddGroupSiftingAux(DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag)
DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key)
DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length)
int st_gen(st_generator *, void *, void *)
static int ddUniqueCompare(int *ptrX, int *ptrY)
static int ddGroupSiftingBackward(DdManager *table, Move *moves, int size, int upFlag, int lazyFlag)
static void ddClearLocal(DdNode *f)
int cuddSymmSiftingConv(DdManager *table, int lower, int upper)
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
static int ddCountRoots(DdManager *table, int lower, int upper)
int cuddNextLow(DdManager *table, int x)
static int zddUniqueCompareGroup(int *ptrX, int *ptrY)
static int ddSiftingBackward(DdManager *table, int size, Move *moves)
static int ddSecDiffCheck(DdManager *table, int x, int y)
int cuddAnnealing(DdManager *table, int lower, int upper)
int cuddZddInitUniv(DdManager *zdd)
void Mtr_FreeTree(MtrNode *node)
static int ddTreeSiftingAux(DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
static int ddGroupMove(DdManager *table, int x, int y, Move **moves)
static int zddGroupSiftingAux(DdManager *table, int x, int xLow, int xHigh)
DdGen * Cudd_FirstCube(DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var)
#define DD_BDD_MAX_EXP_TAG
st_generator * st_init_gen(st_table *)
int cuddZddGetPosVarIndex(DdManager *dd, int index)
static int ddSymmSiftingAux(DdManager *table, int x, int xLow, int xHigh)
Cudd_ReorderingType autoMethodZ
static DdNode * background
static int stopping_criterion(int c1, int c2, int c3, int c4, double temp)
static long shuffleTable[STAB_SIZE]
DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
static int ddGroupSiftingUp(DdManager *table, int y, int xLow, DD_CHKFP checkFunction, Move **moves)
void Mtr_ReorderGroups(MtrNode *treenode, int *permutation)
static void cuddLocalCacheResize(DdLocalCache *cache)
int cuddSwapInPlace(DdManager *table, int x, int y)
static void addVarToConst(DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero)
DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q)
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
static int cuddZddSiftingAux(DdManager *table, int x, int x_low, int x_high)
static Move * zddSwapAny(DdManager *table, int x, int y)
void Cudd_SetMinHit(DdManager *dd, unsigned int hr)
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
static int cuddZddSiftingBackward(DdManager *table, Move *moves, int size)
int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)
struct DdSubtable DdSubtable
static void zddReorderPreprocess(DdManager *table)
int cuddGarbageCollect(DdManager *unique, int clearCache)
static int zddGroupSiftingUp(DdManager *table, int y, int xLow, Move **moves)
long Cudd_ReadNodeCount(DdManager *dd)
#define DD_MAX_SUBTABLE_DENSITY
#define DD_DEFAULT_RECOMB
static int ddPickArbitraryMinterms(DdManager *dd, DdNode *node, int nvars, int nminterms, char **string)
static int ddSiftingAux(DdManager *table, int x, int xLow, int xHigh)
#define MTR_TEST(node, flag)
int cuddSifting(DdManager *table, int lower, int upper)
static Move * ddSiftingUp(DdManager *table, int y, int xLow)
static int ddCheckPermuation(DdManager *table, MtrNode *treenode, int *perm, int *invperm)
static Move * ddSwapAny(DdManager *table, int x, int y)
int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper)
struct DdLocalCache * next
static void zddFindNodeHiLo(DdManager *table, MtrNode *treenode, int *lower, int *upper)
static void debugFindParent(DdManager *table, DdNode *node)
int Cudd_bddVarIsDependent(DdManager *dd, DdNode *f, DdNode *var)
DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g)
static void ddClearFlag(DdNode *f)
#define CUDD_GEN_NONEMPTY
static void ddUpdateInteract(DdManager *table, char *support)
#define DD_MINUS_INFINITY(dd)
static int ddVarGroupCheck(DdManager *table, int x, int y)
unsigned long Cudd_ReadMemoryInUse(DdManager *dd)
int st_insert(st_table *, void *, void *)
static Move * cuddZddLinearUp(DdManager *table, int y, int xLow, Move *prevMoves)
static void freeMatrix(DdHalfWord **matrix)
int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count)
DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar)
static int sift_up(DdManager *table, int x, int x_low)
DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g)
int cuddExact(DdManager *table, int lower, int upper)
unsigned int randomizeOrder
Cudd_VariableType varType
void cuddCacheResize(DdManager *table)
void cuddSetInteract(DdManager *table, int x, int y)
static int ddLinearAndSiftingBackward(DdManager *table, int size, Move *moves)
static Move * ddLinearAndSiftingUp(DdManager *table, int y, int xLow, Move *prevMoves)
int Cudd_EqualSupNorm(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr)
static int PMX(int maxvar)
static int find_best(void)
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
void Cudd_FreeZddTree(DdManager *dd)
int Cudd_PrintLinear(DdManager *table)
#define Cudd_IsComplement(node)
void cuddPrintVarGroups(DdManager *dd, MtrNode *root, int zdd, int silent)
static int zddTotalNumberLinearTr
int cuddNextHigh(DdManager *table, int x)
static void zddVarToConst(DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty)
int cuddGa(DdManager *table, int lower, int upper)
static int ddReorderPreprocess(DdManager *table)
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdHook * postReorderingHook
static void ddFindNodeHiLo(DdManager *table, MtrNode *treenode, int *lower, int *upper)
void cuddSlowTableGrowth(DdManager *unique)
static void fixVarTree(MtrNode *treenode, int *perm, int size)
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
static Move * ddLinearAndSiftingDown(DdManager *table, int x, int xHigh, Move *prevMoves)
CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd)
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
static int computeLB(DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level)
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
#define WEIGHT(weight, col)
static void cuddZddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
#define DD_SIFT_MAX_SWAPS
static DD_INLINE unsigned int ddLCHash(DdNodePtr *key, unsigned int keysize, int shift)
int cuddZddGetPosVarLevel(DdManager *dd, int index)
static int ddLinearUniqueCompare(int *ptrX, int *ptrY)
static void bddFixTree(DdManager *table, MtrNode *treenode)
void Cudd_Quit(DdManager *unique)
static int cuddEstimateCofactor(DdManager *dd, st_table *table, DdNode *node, int i, int phase, DdNode **ptr)
int cuddHeapProfile(DdManager *dd)
Cudd_LazyGroupType varToBeGrouped
struct DdGen::@1::@4 primes
static void cuddLocalCacheAddToList(DdLocalCache *cache)
static void ddPatchTree(DdManager *dd, MtrNode *treenode)
static int array_hash(char *array, int modulus)
int cuddZddSifting(DdManager *table, int lower, int upper)
int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
static int ddResizeTable(DdManager *unique, int index, int amount)
int Cudd_GenFree(DdGen *gen)
int cuddZddUniqueCompare(int *ptr_x, int *ptr_y)
int cuddLinearInPlace(DdManager *table, int x, int y)
int cuddZddNextLow(DdManager *table, int x)
#define DD_BDD_XOR_EXIST_ABSTRACT_TAG
int(* DD_HFP)(DdManager *, const char *, void *)
static Move * cuddZddSymmSifting_down(DdManager *table, int x, int x_high, int initial_size)
static int ddEpdCountMintermAux(DdNode *node, EpDouble *max, EpDouble *epd, st_table *table)
#define cuddIsConstant(node)
static void ddSupportStep(DdNode *f, int *support)
int cuddZddLinearSifting(DdManager *table, int lower, int upper)
static int updateUB(DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper)
static void ddFindSupport(DdManager *dd, DdNode *f, int *SP)
int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)
static Move * ddSymmSiftingDown(DdManager *table, int x, int xHigh)
unsigned long getSoftDataLimit(void)
int Cudd_NextCube(DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
static Move * ddSymmSiftingUp(DdManager *table, int y, int xLow)
#define DD_ADD_EVAL_CONST_TAG
static int cuddZddLinearInPlace(DdManager *table, int x, int y)
static void ddCreateGroup(DdManager *table, int x, int y)
static int updateEntry(DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper)
static int ddReorderPostprocess(DdManager *table)
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
static int bddCheckPositiveCube(DdManager *manager, DdNode *cube)
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
static int zddReorderChildren(DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
#define CUDD_INVERSE_TRANSFORM_MOVE
void cuddLocalCacheClearDead(DdManager *manager)
DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
#define Cudd_Complement(node)
DdLocalCache * localCaches
static st_table * computed
#define DD_MAX_CACHE_TO_SLOTS_RATIO
DdNode * Cudd_Decreasing(DdManager *dd, DdNode *f, int i)
int cuddResizeLinear(DdManager *table)
int st_ptrcmp(const char *, const char *)
static int ddBddShortestPathUnate(DdManager *dd, DdNode *f, int *phases, st_table *table)
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h)
static int ddWindowConv3(DdManager *table, int low, int high)
DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
DdNode * Cudd_ReadOne(DdManager *dd)
void(* MMoutOfMemory)(long)
int Cudd_bddIsVarToBeGrouped(DdManager *dd, int index)
DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E)
static int roulette(int *p1, int *p2)
st_table * st_init_table(ST_PFICPCP, ST_PFICPI)
#define cuddDeallocNode(unique, node)
static int cuddZddLinearBackward(DdManager *table, int size, Move *moves)
DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g)
#define ddCHash2(o, f, g, s)
DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g)
DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var)
int zddTotalNumberSwapping
int cuddLinearAndSifting(DdManager *table, int lower, int upper)
static Move * ddJumpingUp(DdManager *table, int x, int x_low, int initial_size)
DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube)
static DdNode * zdd_subset0_aux(DdManager *zdd, DdNode *P, DdNode *zvar)
static int rand_int(int a)
int Cudd_CheckKeys(DdManager *table)
void cuddHashTableQuit(DdHashTable *hash)
int cuddZddSymmSifting(DdManager *table, int lower, int upper)
static cuddPathPair getShortest(DdNode *root, int *cost, int *support, st_table *visited)
int Cudd_IsGenEmpty(DdGen *gen)
static void ddClearGlobal2(DdManager *table)
#define DD_BDD_LEQ_UNLESS_TAG
int Cudd_zddReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
#define ddEqualVal(x, y, e)
int cuddCacheProfile(DdManager *table, FILE *fp)
int cuddZddSwapInPlace(DdManager *table, int x, int y)
#define ddLCHash1(f, shift)
void cuddLocalCacheClearAll(DdManager *manager)
unsigned int maxReorderings
void cuddRehash(DdManager *unique, int i)
static int cuddEstimateCofactorSimple(DdNode *node, int i)
void Mtr_PrintGroups(MtrNode *root, int silent)
static int array_compare(const char *array1, const char *array2)
void cuddPrintNode(DdNode *f, FILE *fp)
void EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
static int zddTreeSiftingAux(DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
static int zddGroupSifting(DdManager *table, int lower, int upper)
int(* DD_CHKFP)(DdManager *, int, int)
void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep)
int st_add_direct(st_table *, void *, void *)
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
static int restoreOrder(DdManager *table, int *array, int lower, int upper)
int cuddZddAlignToBdd(DdManager *table)
void cuddReclaimZdd(DdManager *table, DdNode *n)
void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0)
int Cudd_bddReadPairIndex(DdManager *dd, int index)
static int ddIsVarHandled(DdManager *dd, int index)
int st_delete(st_table *, void *, void *)
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
static int getLevelKeys(DdManager *table, int l)
#define st_is_member(table, key)
static void ddDissolveGroup(DdManager *table, int x, int y)
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
MtrNode * Mtr_InitGroupTree(int lower, int size)
static int ddExtSymmCheck(DdManager *table, int x, int y)
static void ddClearGlobal(DdManager *table, int lower, int maxlevel)
#define DD_MAX_SUBTABLE_SPARSITY
int Cudd_ReadSize(DdManager *dd)
int cuddZddSymmCheck(DdManager *table, int x, int y)
static cuddPathPair getLargest(DdNode *root, st_table *visited)
static int ddGroupMoveBackward(DdManager *table, int x, int y)
int cuddComputeFloorLog2(unsigned int value)
void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)
#define DD_DEFAULT_RESIZE
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
#define REALLOC(type, obj, num)
int Cudd_bddLeqUnless(DdManager *dd, DdNode *f, DdNode *g, DdNode *D)
int cuddHashTableGenericInsert(DdHashTable *hash, DdNode *f, void *value)
static int ddSymmSiftingBackward(DdManager *table, Move *moves, int size)
struct DdGen::@1::@3 cubes
static int zddGroupMoveBackward(DdManager *table, int x, int y)
DdNode * Cudd_zddDiffConst(DdManager *zdd, DdNode *P, DdNode *Q)
int Cudd_NextNode(DdGen *gen, DdNode **node)
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
int cuddSymmCheck(DdManager *table, int x, int y)
void EpdSubtract3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
static int ddGroupSiftingDown(DdManager *table, int x, int xHigh, DD_CHKFP checkFunction, Move **moves)
DdNode * Cudd_bddAndLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
void Cudd_FreeTree(DdManager *dd)
static int ddSymmGroupMoveBackward(DdManager *table, int x, int y)
static void cuddLocalCacheRemoveFromList(DdLocalCache *cache)
int cuddZddGetNegVarLevel(DdManager *dd, int index)
DdNode *(* DD_CTFP1)(DdManager *, DdNode *)
static double random_generator(void)
#define DD_MAX_REORDER_GROWTH
static void ddReportRefMess(DdManager *unique, int i, const char *caller)
static int ddUpdateMtrTree(DdManager *table, MtrNode *treenode, int *perm, int *invperm)
int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count)
static int ddSetVarHandled(DdManager *dd, int index)
void EpdMakeZero(EpDouble *epd, int sign)
void Cudd_Srandom(long seed)
static int ddWindow4(DdManager *table, int low, int high)
static int ddNoCheck(DdManager *table, int x, int y)
DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
static int ddSymmUniqueCompare(int *ptrX, int *ptrY)
static int ddWindow3(DdManager *table, int low, int high)
void * cuddHashTableGenericLookup(DdHashTable *hash, DdNode *f)
static int cuddZddLinearAux(DdManager *table, int x, int xLow, int xHigh)
void cuddClearDeathRow(DdManager *table)
EpDouble * EpdAlloc(void)
static int ddJumpingAux(DdManager *table, int x, int x_low, int x_high, double temp)
static DdNode * ddBddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f)
#define Cudd_NotCond(node, c)
DdNode * Cudd_bddOrLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
#define DD_PLUS_INFINITY(dd)
int Cudd_DebugCheck(DdManager *table)
static int build_dd(DdManager *table, int num, int lower, int upper)
static int cuddZddSymmSiftingAux(DdManager *table, int x, int x_low, int x_high)
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
static int addMultiplicityGroups(DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask)
static int zddShuffle(DdManager *table, int *permutation)
static int cuddZddSymmSiftingConvAux(DdManager *table, int x, int x_low, int x_high)
static int ddSiftUp(DdManager *table, int x, int xLow)
int cuddTestInteract(DdManager *table, int x, int y)
void Cudd_Deref(DdNode *node)
int Cudd_NextPrime(DdGen *gen, int **cube)
static int ddSymmSiftingConvAux(DdManager *table, int x, int xLow, int xHigh)
static int ddResetVarHandled(DdManager *dd, int index)
void Cudd_OutOfMem(long size)
int st_ptrhash(char *, int)
static double ddCountPathAux(DdNode *node, st_table *table)
int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod)
DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var)
int Cudd_CheckCube(DdManager *dd, DdNode *g)
#define ddLCHash2(f, g, shift)
int Cudd_addLeq(DdManager *dd, DdNode *f, DdNode *g)
void cuddCacheFlush(DdManager *table)
DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g)
static int ddWindowConv2(DdManager *table, int low, int high)
static DdNode * getCube(DdManager *manager, st_table *visited, DdNode *f, int cost)
static int ddPermuteWindow3(DdManager *table, int x)
static Move * cuddZddLinearDown(DdManager *table, int x, int xHigh, Move *prevMoves)
int ddTotalNumberSwapping
struct cuddPathPair cuddPathPair
static int ddWindowConv4(DdManager *table, int low, int high)
int Cudd_RemoveHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
MtrNode * Mtr_MakeGroup(MtrNode *root, unsigned int low, unsigned int high, unsigned int flags)
int cuddResizeTableZdd(DdManager *unique, int index)
static int zddGroupMove(DdManager *table, int x, int y, Move **moves)
static DdNode * zdd_subset1_aux(DdManager *zdd, DdNode *P, DdNode *zvar)
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
DdNode * Cudd_bddIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
static int checkSymmInfo(DdManager *table, DdHalfWord *symmInfo, int index, int level)
DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f)
static void ddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
static int ddPermuteWindow4(DdManager *table, int w)
DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g)
void EpdCopy(EpDouble *from, EpDouble *to)
#define CUDD_LINEAR_TRANSFORM_MOVE
int Cudd_ReadPerm(DdManager *dd, int i)
static DdHalfWord * initSymmInfo(DdManager *table, int lower, int upper)
DdNode * Cudd_addEvalConst(DdManager *dd, DdNode *f, DdNode *g)
void cuddFreeTable(DdManager *unique)
static void ddRehashZdd(DdManager *unique, int i)
static int zddReorderPostprocess(DdManager *table)
static int cuddHashTableResize(DdHashTable *hash)
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
static int cuddZddSymmSiftingBackward(DdManager *table, Move *moves, int size)
DdNode * cuddZddComplement(DdManager *dd, DdNode *node)
DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
static int cuddNodeArrayRecur(DdNode *f, DdNodePtr *table, int index)
static int ddShuffle2(DdManager *table, int *permutation)
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
DdNode * cuddBddXorExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
int cuddInitLinear(DdManager *table)
static int dp2(DdManager *dd, DdNode *f, st_table *t)
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
int Cudd_bddIsVarToBeUngrouped(DdManager *dd, int index)
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
int cuddSymmSifting(DdManager *table, int lower, int upper)
void cuddReclaim(DdManager *table, DdNode *n)
int cuddZddP(DdManager *zdd, DdNode *f)
static long shuffleSelect
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
int cuddZddGetNegVarIndex(DdManager *dd, int index)
void cuddZddFreeUniv(DdManager *zdd)
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
static int zdd_group_move_backward(DdManager *table, int x, int y)
static DdNode * cuddUniqueLookup(DdManager *unique, int index, DdNode *T, DdNode *E)
DdNodePtr * cuddNodeArray(DdNode *f, int *n)